From 7c74396eb25da8b64d70629faaa2a89a74d48978 Mon Sep 17 00:00:00 2001 From: David Arias Date: Wed, 14 Oct 2026 10:35:39 -0500 Subject: [PATCH 1/2] Prove controller conservation for native source-code transfers --- .../native-controller-congruence/ARCHIVE.json | 18 + .../PREDECESSOR.json | 19 + .../native-controller-congruence/README.md | 313 ++++++++++++++ .../native-controller-congruence/RESULT.json | 57 +++ .../native-controller-congruence/SOURCES.json | 36 ++ .../native-controller-congruence/TASK.json | 124 ++++++ .../VALIDATION.json | 55 +++ .../native-controller-congruence/VERIFY.json | 35 ++ .../references/NOTICE.md | 50 +++ .../references/UNIT-TRANSFER-PROOF.md | 218 ++++++++++ .../test_verify.py | 398 ++++++++++++++++++ .../native-controller-congruence/verify.py | 213 ++++++++++ 12 files changed, 1536 insertions(+) create mode 100644 research/native-controller-congruence/ARCHIVE.json create mode 100644 research/native-controller-congruence/PREDECESSOR.json create mode 100644 research/native-controller-congruence/README.md create mode 100644 research/native-controller-congruence/RESULT.json create mode 100644 research/native-controller-congruence/SOURCES.json create mode 100644 research/native-controller-congruence/TASK.json create mode 100644 research/native-controller-congruence/VALIDATION.json create mode 100644 research/native-controller-congruence/VERIFY.json create mode 100644 research/native-controller-congruence/references/NOTICE.md create mode 100644 research/native-controller-congruence/references/UNIT-TRANSFER-PROOF.md create mode 100644 research/native-controller-congruence/test_verify.py create mode 100644 research/native-controller-congruence/verify.py diff --git a/research/native-controller-congruence/ARCHIVE.json b/research/native-controller-congruence/ARCHIVE.json new file mode 100644 index 0000000000..43d2774e17 --- /dev/null +++ b/research/native-controller-congruence/ARCHIVE.json @@ -0,0 +1,18 @@ +{ + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "members": { + "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz": { + "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" + }, + "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz": { + "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "payload_sha256": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3" + }, + "candidate/strict/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": { + "sha256": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "payload_sha256": "8904bbbf46dfbf1c6df0e43479a23913fc59a410e879188112e88f16c850ede8" + } + } +} diff --git a/research/native-controller-congruence/PREDECESSOR.json b/research/native-controller-congruence/PREDECESSOR.json new file mode 100644 index 0000000000..bd69d2b722 --- /dev/null +++ b/research/native-controller-congruence/PREDECESSOR.json @@ -0,0 +1,19 @@ +{ + "sources": [ + { + "upstream_path": "research/native-source-codes/UNIT-TRANSFER-PROOF.md", + "local_path": "references/UNIT-TRANSFER-PROOF.md", + "commit": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", + "sha256": "2e83366264c108b2c9f371a13b379093813d99060b88858c640a7c403bbd3c3d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1862" + }, + { + "upstream_path": "research/native-source-codes/NOTICE.md", + "local_path": "references/NOTICE.md", + "commit": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", + "sha256": "d86f31a4c0bafd4271fe0c0e087a7fc1cd72d5b705e3739c4ba3e9241b7ba3f9", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1862" + } + ], + "executed_predecessor_code": false +} diff --git a/research/native-controller-congruence/README.md b/research/native-controller-congruence/README.md new file mode 100644 index 0000000000..a8e7abf699 --- /dev/null +++ b/research/native-controller-congruence/README.md @@ -0,0 +1,313 @@ +# A determinant obstruction for native source-code controllers + +**Scoped structural result; no new supplier or kappa.** PR1862 supplies exact +local identity transfers that store an eight-coordinate centre query in +existing data fields. Its remaining obstacle is a complete controller that +removes the source code while delivering the required data endpoint. This +package rules out an unbounded class of proposed controllers, rather than +searching words only up to a length cutoff. + +For one fixed source code, every completed controller built from PR1862's +forward/backward transfers, their inverses, and arbitrary invertible scalar +mixing of whole port banks must have **signed code winding divisible by six**. +The statement allows any number of data banks and restored dirty auxiliary +banks, arbitrary dyadic scales and signs, and arbitrarily long words. It rules +out the inherited nine-call, four-pair scalar skeleton, whose winding is -1, +under this fixed-code substitution. Merely repeating a fixed code until its +sixth power is the identity does not remove this controller constraint. + +A complementary result allows a different admissible source code at each of +three calls. In an F-B-F exchange, the unwanted diagonal block has rank at +least eight for **every** choice of those charts with the retained R and K. +Changing the selected rows inside this three-call architecture cannot remove +the defect. This is stronger than testing the predecessor's one fixed chart. + +These are controller-interface obstructions. Port-dependent scalar maps, +physical changes of chart, new clean workspace, and paid repairs remain +outside the first theorem. The second theorem does not include interleaved +bank mixing or arbitrary native chart transports. Neither result is a lower +bound for all multiplication algorithms or a rejection of PR1862's valid +local construction. + +## The pinned local interface + +Write a port bank as an n-vector. PR1862 works over the dyadic coefficient +ring with maps R of size r by n, K of size n by r, and maps P,L satisfying + +```text +RP = I, LK = I, LP = 0. +M = RK, Z = K - P(M-I), Q = R-L. +G = (I-PL)(I+ZQ) = I + ZQ - PR. +G^-1 = I + PL - ZR. +``` + +Its completed local content maps, with the native frames and charges still +required, are + +```text +B_G(x,y) = (x-y, Gy), +F_G(x,y) = (G^-1 x, y+G^-1 x). +``` + +The actual source has n=112, r=8, K=R^T/4 and RK=14I. The selected sets are + +```text +A = [0,7,20,27,36,46,57,111], +T = [21,37,47,76,81,87,92,110]. +``` + +The identities QP=LZ=I and QZ=LP=0 split each bank uniquely into + +```text +y = w + Pu + Zv, Qw=Lw=0. +G: (w,u,v) -> (w,-v,u+v). +``` + +Consequently G fixes a 96-dimensional subspace and acts on eight +two-dimensional sections by `[[0,-1],[1,1]]`. Its minimal polynomial over Q +is exactly + +```text +f(t) = (t-1)(t^2-t+1), +``` + +not just a polynomial that happens to annihilate G. Both summands are +nonzero, and the two factors are coprime. In particular, the algebra Q[G] +is faithfully represented by `A = Q[t]/(f)` and t has order exactly six. +The local construction and these identities retain PR1862's attribution. + +## Theorem 1: balance for every word in one fixed chart + +Take any finite number b of whole n-port banks. Each bank initially has +arbitrary independent contents. An auxiliary bank, if present, must be +restored for every initial value. The permitted controller operations are: + +1. A B_G or F_G transfer on any ordered pair of distinct banks, or its true + inverse, with the same G throughout. +2. Any invertible scalar bank map `S tensor I_n`, where `S` is a b by b + matrix over Q. This includes the inherited bridges, signs, permutations, + arbitrary rational scales, and their dyadic special cases. All scalar + work must still be charged in a physical implementation. + +Require the completed map on all banks to be a specified invertible scalar +bank map `T tensor I_n`. Restored auxiliary banks contribute identity blocks +to T. The theorem also permits scalar cross-bank terms if they are explicitly +part of the required endpoint. There is no controller-level CLEAR or +assumption that an auxiliary bank begins clean. + +Assign winding +1 to B_G and F_G^-1, and -1 to F_G and B_G^-1. Let w be the +sum over the word. **Then 6 divides w.** + +**Proof.** Work with b by b matrices over the commutative algebra A. The +nontrivial two-bank blocks are + +```text +B(t) = [[1,-1],[0,t]], det B = t, +F(t) = [[t^-1,0],[t^-1,1]], det F = t^-1. +``` + +Inverses have reciprocal determinants. Embedding a block in any pair of +banks leaves its determinant unchanged. Let delta be the product of the +determinants of all scalar operations; delta is a nonzero rational number. +Multiplicativity of determinants gives + +```text +det(controller) = delta * t^w = det(T) in A. +``` + +Evaluation at t=1 yields delta=det(T). Cancel that nonzero rational number. +Evaluation at a primitive sixth root zeta, which is another homomorphism +from A, now gives zeta^w=1. Therefore w is a multiple of six. This proof is +independent of word length and of the number of banks. It does not use a +finite search as a universal inference. + +Every macro occurrence contributes an odd integer, +1 or -1, so **an odd +number of these macro calls cannot have the required scalar endpoint**, even +if inverse calls are allowed. Divisibility is only necessary: a word of +winding zero or six need not be a correct controller. + +The ordinary determinant of the full 112b-dimensional rational matrix would +miss this constraint: det(G)=1. The useful determinant is over Q[G], whose +fixed and cyclotomic components must both have the requested endpoint. + +**Corollary: coherent changes of basis do not evade the constraint.** At +boundary k let `H_k=diag(U_k,1,...,U_k,b)` be an arbitrary invertible +bankwise change of coordinates. Suppose each physical operation is exactly +`H_k N_k H_(k-1)^-1`, where N_k is one of the normalized operations above. +A local code that keeps its coordinate chart has the form `U_i G U_i^-1`, +and a scalar bridge within a fixed chart has transport `a U_i U_j^-1`. +If the charts also change during the operation, the incoming factors are +instead `U_(k-1),i^-1` and `U_(k-1),j^-1`, respectively, as in the displayed +general formula. A passive change of coordinates has N_k=I. The physical product telescopes to + +```text +H_m (N_m ... N_1) H_0^-1. +``` + +If the required endpoint is `H_m (T tensor I_n) H_0^-1`, including the +specified final gauges and complete source restoration, the same proof +forces 6 to divide w. The matrices U need not commute with G. This is an +exact conjugacy condition, not a claim that the actual native routing maps +satisfy it. A proposed escape must change the normalized operation or its +endpoint contract; relabeling the same code coherently is insufficient. + +## Application to the inherited nine-call scalar skeleton + +The retained four-pair construction starts with F_0 and then uses +`B_0,F_0,B_1,F_1,B_2,F_2,B_3,F_3`, with scalar bridges and a final signed +exchange. It therefore contains four B calls and five F calls. Bridges and +the signed exchange are scalar whole-bank maps; they cannot change w=-1. + +Substituting one fixed PR1862 source code into this skeleton cannot give its +required scalar identity, regardless of how its scalar whole-bank controller +is redesigned. This covers all whole-bank scalar repairs at the same nine +macro calls, not only the displayed bridge constants. More generally, no +odd-call controller in the stated class works. + +This is a statement about a fixed-code interpretation of the inherited +scalar skeleton. Actual native stages have port-dependent address routes +and frame changes; the theorem does not identify those different physical +charts with a single G. It also does not establish a lower bound on the +number of children in a successful replacement. In particular, a true +inverse macro may undo native frame progress, so an algebraic cancellation +fixture is not an admitted supplier. + +## Theorem 2: a rank-eight defect for every three-chart F-B-F exchange + +Now fix R and K but allow each chart s to choose its own P_s,L_s, satisfying +the same three identities. Let G_s be its resulting code. Ordered +multiplication gives, without assuming M=RK is central, + +```text +R G_s K = M-I, R G_s^-1 K = I. +``` + +For arbitrary admissible charts a,b,c, the exact three-call content matrix is + +```text +F_c B_b F_a = [[0, -G_c^-1], + [G_b G_a^-1, G_b-G_c^-1]]. +``` + +The desired signed exchange has zero lower-right block. Let +`D=G_b-G_c^-1`. Then + +```text +R D K = M-2I. +``` + +Over a field, rank(D) is at least rank(M-2I). For the actual RK=14I over Q +or Q(i), this gives **rank(D) >= 8**, independently of all three selected +chart choices. No inverse of M is used. The same statement cannot be +inferred in characteristics that annihilate 12. + +Separate invertible input and output gauges on each bank multiply D on its +left and right by invertible maps and preserve its nonzero rank. Thus these +endpoint gauges cannot turn the exchange into a matrix with that block +zero. This observation does not allow interleaved bank mixing, changes to +R,K, operator-valued chart transport, or a paid cancellation of D. + +The rank bound concerns the unwanted data map. It is **not** an assertion +that exactly eight native children implement its cancellation, nor a lower +bound of eight for arbitrary physical implementations. An admissible repair +still needs its source access, frame moves, restoration and full invoice. + +## Reproduction and evidence boundary + +From the repository root: + +```sh +python3 -I -B research/native-controller-congruence/verify.py +python3 -I -O -B research/native-controller-congruence/test_verify.py +python3 scripts/research_package.py --package research/native-controller-congruence --check-only +python3.12 scripts/research_package.py --package research/native-controller-congruence +``` + +The written determinant proof establishes the unbounded statement. The +exact verifier checks its finite algebraic premises and meaningful controls; +these finite checks are not a proof-assistant formalization. The package +records its checked inputs, receipt and failure controls separately. The +source record and predecessor references are bound in [SOURCES.json](SOURCES.json), +and [TASK.json](TASK.json) records the changed scope from `centre-path-sharing`. +The predecessor proof and notice are exact text copies under `references/`, +with their original relative links referring to the pinned upstream package. +No predecessor executable is imported. + +The source-bound verifier reads three pinned members of the selected PR1094 +replay archive. Its local word and program payloads are byte-identical to the +PR1042 inputs consumed by PR1862. It replays the **112 source columns only** +up to the forward centre cut, derives R,K,P,L and the 96+16 decomposition, +and checks `RDK=12I_8` for all four pairs of the actual A/T and swapped T/A +charts. The retained parent `GLOBAL-TEMPLATE` supplies only the exact +`(pair, reverse, stage)` recipe; its older embedded provider program is not +executed. This is not a replay of current helper or native endpoint behavior. + +The separate dense rational checker imports neither `verify.py` nor +predecessor code. Its 12 tests include 108 macro/scalar interleavings over +two, three and four banks; inverse and sign/scale controls; a six-call +algebraic exchange; noncentral-M and changed-chart rank fixtures; and +isolated CLI tests that reject changed result, archive-pin and predecessor +text inputs. The six-call example proves that the condition is only +necessary and that legal signs must be included; it does not establish +useful native frame progress or an affordable supplier. + +The registered replay passed on CPython 3.12.14. The primary verifier also +passed with `-O`, and the repository research-workflow suite passed 45 tests +with three platform skips. Commands and environment are in +[VALIDATION.json](VALIDATION.json). + +No new native words, complete supplier, improved moment, physical runtime +bound or multiplication theorem is certified. Full selected-supplier cold +replay, native routing, hosting, tape and precision admission are not claims +of this package. The selected frontier and frozen source artifacts remain +unchanged. + +## Open next questions + +- **A code-balanced controller with real frame progress.** The winding + condition rules out odd call counts but does not build an even one. A + feasible first step is an exact bank controller whose winding is zero or + six, followed by a typed native-frame replay and full child profile. + The blocker is useful coordinate progress: cancellation by a true inverse + can erase the very transformation the supplier needs to perform. +- **A priced escape through actual chart transport.** PR1862's law + `R_t(G_t^-1 U G_s)=V_R R_s` is conditional on the selected transport. + Derive one actual stage transition, including its port-dependent address + maps, and check full-source restoration as well as query transport. + Such maps need not lie in Q[G], which is precisely why the present + determinant obstruction does not settle that route. +- **Repair the universal three-chart defect.** The equation `RDK=12I` + identifies an eight-dimensional unavoidable observable. First factor D + for one chosen pair of charts and find a legal native cut for a paid + correction. The blocker is an implementable and affordable correction, + not the rank computation alone. + +Port-dependent scalar mixing or newly admitted clean workspace changes the +first theorem's alphabet. These are explicit reopening conditions, not +operations proved impossible here. No further random seed or longer search +inside the excluded odd-call class can remove its determinant obstruction. + +## Predecessors, distinction and credit + +- Ali Romman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862), + pinned at `bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f`, supplies the valid + ordered-ring source code, native identity transfers, eight-row repair + bound, exact fixed-chart order six, and its fixed-chart F-B-F failure + control. This package does not claim any of those as new. Its additions + are the all-length determinant constraint with arbitrary whole-bank + scalar mixing, and the three-chart rank bound for all admissible P,L. +- Chafik Boukhalfa's [PR1877](https://github.com/CrocSwap/integer-mult-bounds/pull/1877) + proves an endpoint-support tradeoff and fixed native-frame obstruction + for the original clean-J logger. It leaves changed codes and later or paid + native transitions open. The present contribution concerns the later + identity-target codes and completed bank controllers, rather than + reproving its source-support or native-frame statement. +- The retained four-pair scalar chain and native geometry come from the + split-centres/gauge44 construction and its inherited authors. The pinned + PR1042/PR1094 lineage retains Jeremy Kothe, Chafik Boukhalfa, Rohan Arun, + Hao Yan, icekylinx, NewBArch and the source-specific notices. No historical + construction or selected evidence is modified. + +Prepared by David Arias with substantial OpenAI Codex assistance in scoping, +proof derivation, exact verification and review. Independent agent review is +not independent human review. New work is Apache-2.0. diff --git a/research/native-controller-congruence/RESULT.json b/research/native-controller-congruence/RESULT.json new file mode 100644 index 0000000000..2ca90fca46 --- /dev/null +++ b/research/native-controller-congruence/RESULT.json @@ -0,0 +1,57 @@ +{ + "status": "PASS_NATIVE_CONTROLLER_CONGRUENCE", + "selected_source_query_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213", + "ports": 112, + "query_rank": 8, + "fixed_dimension": 96, + "minimal_polynomial_low_to_high": [ + -1, + 2, + -2, + 1 + ], + "active_powers_0_to_5": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + -1, + 1 + ], + [ + -1, + 0 + ], + [ + 0, + -1 + ], + [ + 1, + -1 + ] + ], + "recipe": [ + "F", + "B", + "F", + "B", + "F", + "B", + "F", + "B", + "F" + ], + "signed_winding": -1, + "required_winding_modulus": 6, + "changed_chart_pairs_checked": 4, + "changed_chart_defect_compression": "12 I_8", + "changed_chart_defect_rank_lower_bound": 8, + "selected_frontier_changed": false, + "coverage": "Source-column prefix and scalar-controller algebra; no native or all-size cold replay." +} diff --git a/research/native-controller-congruence/SOURCES.json b/research/native-controller-congruence/SOURCES.json new file mode 100644 index 0000000000..566d52464d --- /dev/null +++ b/research/native-controller-congruence/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "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": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ] +} diff --git a/research/native-controller-congruence/TASK.json b/research/native-controller-congruence/TASK.json new file mode 100644 index 0000000000..139d04a9e7 --- /dev/null +++ b/research/native-controller-congruence/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 3, + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "A determinant conservation law for arbitrary-length controllers of PR1862 identity transfers and whole-bank scalar bridges; independent changing-chart three-call rank obstruction.", + "scope_change_reason": "The first suggested coverage-law card overlaps Discussion1587 and PRs1825/1889/1900/1936. The second suggested centre-path card is narrowed to the native source-code controller missing from PR1862, a prerequisite for replacing the paid centre path. This proves an obstruction rather than proposing a centre charge.", + "bottleneck_link": "PR1862 is a native candidate for removing the 64-per-call centre path; a full-source-restored controller is still missing. Test the entire inherited scalar-controller class before attempting native admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact controller law, source-bound selected-word fixture and independent controls; do not manufacture a kappa or cold-replay claim.", + "outcome": "negative-result", + "evidence": "README proves the unbounded determinant law and universal three-chart rank bound. RESULT.json binds exact selected source columns, the112-port chart decomposition, nine-stage orientation census and four actual chart-pair compressions. test_verify.py independently checks dense rational interleavings, inverses, legal signs/scales, six-call positive control and failing hypotheses.", + "author": "David Arias, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof, implementation and independent agent checking; no independent human review.", + "open_questions": [ + { + "question": "Can a code-balanced even controller make useful native frame progress?", + "why_it_matters": "The conservation law is necessary, not sufficient; useful progress could still realize the centre-path candidate.", + "first_step": "Construct a zero-winding bank word, then replay its typed native entry and exit frames.", + "blocked_by": "True inverse cancellations may undo the required coordinate advance." + }, + { + "question": "Can one actual priced chart transition escape the normalized scalar controller algebra?", + "why_it_matters": "Physical port-dependent transports are excluded from the determinant theorem and may permit a real implementation.", + "first_step": "Derive a selected source transport and check full-source restoration, not only query transport.", + "blocked_by": "Nonuniform address maps and frame conversions must be implemented and charged." + }, + { + "question": "Can the rank-eight three-chart defect be repaired affordably?", + "why_it_matters": "Every three-call exchange with the same R,K retains an observable eight-dimensional error.", + "first_step": "Factor D for a chosen pair of admissible charts and locate a legal native correction cut.", + "blocked_by": "Rank alone is not an implementation or a recursive child invoice." + } + ], + "selection": { + "seed": "5793b6b4f3a4e9b073ecf21eab76559f", + "track": "recursive-interfaces", + "scope_key": "184695337cedab03152e", + "track_override_reason": "User requested a significant structural contribution rather than marginal refinements." + }, + "coordination": "Live read-only overlap checks; no public coordination post because the user-supplied AGENTS instructions restrict those without authorization.", + "optimistic_budget": "The existing centre-free relaxation is 2.80x the fixed-word primitive ceiling; this necessary controller test precedes any realized budget. No altered profile is priced or accepted.", + "overlap": { + "searched_at": "2026-10-14T15:33:43.867059+00:00", + "terms": [ + "code winding", + "controller determinant", + "native source code", + "source-code controller", + "M-2I", + "three-chart" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T15:32:26.111961+00:00", + "complete_pagination": true, + "records": 538 + }, + "discussions": { + "fetched_at": "2026-10-14T15:33:43.779050+00:00", + "complete_pagination": true, + "records": 599 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "remote_matches_for_final_terms": 0, + "closest_predecessors": [ + { + "pr": 1862, + "head": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", + "delta": "Adds all-length scalar-controller conservation and arbitrary-chart FBF rank obstruction to valid native local words." + }, + { + "pr": 1877, + "head": "6d455d2d71eb35ecf8e562711e5f719b994fe3f3", + "delta": "Identity-target source codes rather than original clean-J logger support/commutant." + } + ] + }, + "submission_base": "ae95f60feec79897b153dba6459bb3f9fd4d7b8e" +} diff --git a/research/native-controller-congruence/VALIDATION.json b/research/native-controller-congruence/VALIDATION.json new file mode 100644 index 0000000000..521b2037a2 --- /dev/null +++ b/research/native-controller-congruence/VALIDATION.json @@ -0,0 +1,55 @@ +{ + "checked_at_utc": "2026-10-14T15:36:19.115360+00:00", + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "submission_base": "ae95f60feec79897b153dba6459bb3f9fd4d7b8e", + "commands": [ + { + "argv": [ + "python3.12", + "scripts/research_package.py", + "--package", + "research/native-controller-congruence" + ], + "exit_code": 0, + "stdout": "CHECK Exact source-column prefix, actual source-code split, four changed-chart rank witnesses, nine-call orientation census and recorded receipt.\n{\n \"status\": \"PASS_NATIVE_CONTROLLER_CONGRUENCE\",\n \"selected_source_query_sha256\": \"70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213\",\n \"ports\": 112,\n \"query_rank\": 8,\n \"fixed_dimension\": 96,\n \"minimal_polynomial_low_to_high\": [\n -1,\n 2,\n -2,\n 1\n ],\n \"active_powers_0_to_5\": [\n [\n 1,\n 0\n ],\n [\n 0,\n 1\n ],\n [\n -1,\n 1\n ],\n [\n -1,\n 0\n ],\n [\n 0,\n -1\n ],\n [\n 1,\n -1\n ]\n ],\n \"recipe\": [\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\"\n ],\n \"signed_winding\": -1,\n \"required_winding_modulus\": 6,\n \"changed_chart_pairs_checked\": 4,\n \"changed_chart_defect_compression\": \"12 I_8\",\n \"changed_chart_defect_rank_lower_bound\": 8,\n \"selected_frontier_changed\": false,\n \"coverage\": \"Source-column prefix and scalar-controller algebra; no native or all-size cold replay.\"\n}\nCHECK Independent dense rational determinant, arbitrary bank mixing/inverse controls, varying-chart defect and six-call positive control.\nPASS_REGISTERED_RESEARCH_PACKAGE research/native-controller-congruence outcome=negative-result\n", + "stderr": "............\n----------------------------------------------------------------------\nRan 12 tests in 1.958s\n\nOK\n" + }, + { + "argv": [ + "python3.12", + "-I", + "-O", + "-B", + "research/native-controller-congruence/verify.py" + ], + "exit_code": 0, + "stdout": "{\n \"status\": \"PASS_NATIVE_CONTROLLER_CONGRUENCE\",\n \"selected_source_query_sha256\": \"70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213\",\n \"ports\": 112,\n \"query_rank\": 8,\n \"fixed_dimension\": 96,\n \"minimal_polynomial_low_to_high\": [\n -1,\n 2,\n -2,\n 1\n ],\n \"active_powers_0_to_5\": [\n [\n 1,\n 0\n ],\n [\n 0,\n 1\n ],\n [\n -1,\n 1\n ],\n [\n -1,\n 0\n ],\n [\n 0,\n -1\n ],\n [\n 1,\n -1\n ]\n ],\n \"recipe\": [\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\",\n \"B\",\n \"F\"\n ],\n \"signed_winding\": -1,\n \"required_winding_modulus\": 6,\n \"changed_chart_pairs_checked\": 4,\n \"changed_chart_defect_compression\": \"12 I_8\",\n \"changed_chart_defect_rank_lower_bound\": 8,\n \"selected_frontier_changed\": false,\n \"coverage\": \"Source-column prefix and scalar-controller algebra; no native or all-size cold replay.\"\n}\n", + "stderr": "" + }, + { + "argv": [ + "python3.12", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_*.py" + ], + "exit_code": 0, + "stdout": "CHECK Scoped test fixture\nPASS_REGISTERED_RESEARCH_PACKAGE research/fixture outcome=partial\nCHECK Scoped test fixture\n", + "stderr": "...........................Traceback (most recent call last):\n File \"\", line 1, in \nAssertionError: invalid fixture\nTraceback (most recent call last):\n File \"\", line 1, in \nAssertionError: invalid fixture\n.........sss......\n----------------------------------------------------------------------\nRan 45 tests in 4.608s\n\nOK (skipped=3)\n" + } + ], + "unrun": [ + "Selected complete make frontier1094-verify", + "Native endpoint or compiler replay", + "Full multiplication theorem or proof-assistant verification" + ], + "review": "Two separate agents checked proof scope and actual source extraction; no independent human review.", + "interpreter_note": "Commands use the portable python3.12 name for the recorded CPython 3.12.14 bundled runtime.", + "expected_negative_test_stderr": "The two invalid-fixture AssertionError tracebacks in the research-workflow suite are expected failure-control subprocesses; the suite exits zero." +} diff --git a/research/native-controller-congruence/VERIFY.json b/research/native-controller-congruence/VERIFY.json new file mode 100644 index 0000000000..905a0fad83 --- /dev/null +++ b/research/native-controller-congruence/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/community-batch1099-review.md", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source-column prefix, actual source-code split, four changed-chart rank witnesses, nine-call orientation census and recorded receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent dense rational determinant, arbitrary bank mixing/inverse controls, varying-chart defect and six-call positive control." + } + ] +} diff --git a/research/native-controller-congruence/references/NOTICE.md b/research/native-controller-congruence/references/NOTICE.md new file mode 100644 index 0000000000..24461eddc1 --- /dev/null +++ b/research/native-controller-congruence/references/NOTICE.md @@ -0,0 +1,50 @@ +# Source attribution and license + +New research, code, and verification used substantial OpenAI Codex +assistance under the user's direction. Separate agents developed the +input construction and reviewed its algebra, native phases, and literal +programs. No independent human review is claimed. New material uses the +repository's Apache-2.0 license. + +The package reads immutable source objects at commit +`bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. It does not change the frozen +source archive or copy a predecessor package. Exact source pins are in +[SOURCES.json](SOURCES.json). The original notices are retained as exact +files under `notices/`. + +The local word comes from the gauge44 lineage. Its +[notice](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots-t16/NOTICE.md) +credits @icekylinx, with OpenAI GPT-6 Astra assistance, for the source +gauge and related local construction. The +[construction notice](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots-t16/construction/NOTICE.md) +preserves the factory, K-triangle, porting, joint-prefix, and HPE lineage. + +The retained +[t16 notice](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots-t16/t16/NOTICE.md) +credits Hao Yan (@FanPUYen) for the integration; Jeremy Kothe +(@jeremykothe2) for the [PR #799](https://github.com/CrocSwap/integer-mult-bounds/pull/799) +local supplier; and Chafik Boukhalfa (@chafreaky) for the +[PR #741](https://github.com/CrocSwap/integer-mult-bounds/pull/741) +frame work. These sources and their earlier attribution are retained +inputs, not new results of this package. Name-to-account evidence is in +the pinned +[contributor record](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/CONTRIBUTORS.md). + +The complete +[upstream notice](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots-t16/UPSTREAM-NOTICE.md) +retains DreamingOfClouds, earlier cold-end and joint-prefix work, other +contributors, source pins, licenses, and AI disclosures. It is copied +without edits. The selected slot-word lineage also credits @rohanarun +for [PR #987](https://github.com/CrocSwap/integer-mult-bounds/pull/987) +and NewBArch for [PR #869](https://github.com/CrocSwap/integer-mult-bounds/pull/869) +in the pinned +[local README](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/gauge44-slots/README.md). +NewBArch is the credited source name; no account identity is inferred. + +The portable source loader, sparse replay, and exact native interpreter +come from this centre-encoding campaign. They retain the same source +objects used in [PR #1719](https://github.com/CrocSwap/integer-mult-bounds/pull/1719), +but this package does not depend on that PR being merged. The new verifier +does not import the source-code producer or the exploratory native +compiler. The historical global owner map and final invoice are not +replayed or improved by this local package. diff --git a/research/native-controller-congruence/references/UNIT-TRANSFER-PROOF.md b/research/native-controller-congruence/references/UNIT-TRANSFER-PROOF.md new file mode 100644 index 0000000000..c04a8613f9 --- /dev/null +++ b/research/native-controller-congruence/references/UNIT-TRANSFER-PROOF.md @@ -0,0 +1,218 @@ +# Eight-row identity transfers with a full-query source code + +The historical complex supplier has a local backward content map +`(x,y,h,c) -> (x-Jy,y,h,0)`, where `J=I-KR`. This construction changes +that map to `(x-y,Gy,h,0)`. It stores the original full centre query in +eight selected source fields. A forward companion gives +`(G^-1x,y+G^-1x,h,0)`. + +Each complete word restores all 480 arbitrary helpers. It adds eight +rank-one native children, 16 address maps, and no array field. Its scalar +allowance is 217898 real primitives per array coordinate. The source code +has order six in one fixed chart. The complete supplier and kappa bound +are unchanged: routed composition, source removal, and the full recursive +invoice remain open. + +## An ordered-ring construction + +Work over a unital ring. All products have the stated order. Let R have +r rows and n columns, and let K have n rows and r columns. Suppose +supplied maps P and L satisfy + +```text +RP=I, LP=0, LK=I. +``` + +Set `M=RK`, `J=I-KR`, and + +```text +Z=K-P(M-I), Q=R-L. +``` + +Then `RZ=LZ=QP=I`, `QZ=0`, and `JZ=-P(M-I)`. Define + +```text +G=(I-PL)(I+ZQ)=I+ZQ-PR, +G^-1=(I-ZQ)(I+PL)=I+PL-ZR. +``` + +Both factors are units: `(PL)^2=(ZQ)^2=0`. Direct multiplication gives + +```text +LG=R, RG=Q, +C=JG-I=-P[R+(M-I)Q]. (1) +``` + +Thus C has support only on the support rows of P. No inverse of M or +M-I occurs. The construction does not require M to be scalar or central. + +For any source y, put `u=Qy`, `v=Ly`, and `w=y-Pu-Zv`. These give the +direct sum `y=w+Pu+Zv`, with `Qw=Lw=0`. The code fixes w and sends +`(u,v)` to `(-v,u+v)`. Its matrix on the two section images is +`[[0,-I],[I,I]]`. Its cube is minus I there, so `G^6=I` on the full +source. Over the actual dyadic ring and r>0, its order is exactly six. +Positive characteristic can reduce the order. + +## The two local words + +For the backward word, first add Cy to x, then apply G to y, then run +the retained clean-J backward core. Equation (1) gives + +```text +x+Cy-JGy=x-y. +``` + +The complete map is `(x-y,Gy,h,0)`. The target uses the identity matrix +on all n source fields, not only on a quotient by the selected rows. + +For the forward word, run the clean core `(x,y+Jx,h,0)`. At its complete +exit, apply G inverse to x and denote the result by x'. The target is +`y+JGx'=y+x'+Cx'`. Subtract Cx' from the selected target rows. The result +is `(G^-1x,y+G^-1x,h,0)`. + +These words are companions, not inverse calls. An inverse of the +backward content map is `(x+G^-1y,G^-1y)`. The emitted calls also clear +owned private inputs; they do not restore those initial values. + +## The actual scalar and native interface + +The pinned supplier has `K=R^T/4` and `RK=14I`. It uses disjoint sets + +```text +A=[0,7,20,27,36,46,57,111], +T=[21,37,47,76,81,87,92,110]. +``` + +Both minors satisfy `R_A R_A^T=R_T R_T^T=4I`. Take +`P=iota_A R_A^-1` and `L=R_T selector_T`. The backward source output +has `Y_T'=R_T^-1 RY`, so it stores the full original query in existing +fields. The physical endpoints remain + +```text +X_p: C_p -> FULL, +Y_p: I -> FULL C_p^-1. +``` + +The backward correction is before every retained entry adapter. Form +each row of CY in owned C0 at I, apply the intrinsic positive C_p to C0, +add it into X_p, and clear C0. This uses one rank-one child on each A +port. The exact input recipes include the scalar phase; a binary +subspace representative alone is insufficient. + +Next apply `I+ZQ` to Y with one private accumulator. Read a full row +q_k Y before its scatter by column z_k. Since every `q_i z_k=0`, each +completed scatter preserves every later query. Clear C0 after each row. +Finally apply `I-PL`: the A fields read the disjoint T fields. This last +factor has 32 signed-half ADDs. + +For the forward word, every retained core event runs first. At FULL, +apply `I+PL` to X, then the serial inverse of `I+ZQ`. Form each row of +`-CX'` in C0 at FULL. Apply the intrinsic inverse C_p to that copy, add +it into Y_p at `FULL C_p^-1`, and clear C0 back to I. C_p commutes with +FULL in this pinned interface. The certificate gives the exact inverse +line recipe, including its translation and scalar phase. + +All 480 helper outputs keep their original native transforms. Helper +restoration in the displayed maps refers to canonical contents. The +source query fields keep their individual native endpoint frames; +clean query contents do not provide free common-frame access. + +## Exact local cost + +| Part | Real scalar primitives | +| --- | ---: | +| Retained clean core | 202138 | +| Source code or its inverse | 9056 | +| Selected target correction | 6704 | +| Complete word | 217898 | + +Each full word has 20694 ADDs, 707 SCALEs, and 48 CLEARs. It uses only +the existing C0 for its added work. All eight owned private fields finish +at zero. The complete native profile is + +```text +{1:2420, 2:418, 3:432, 4:142, 5:82} +``` + +Its rank mass is 5530, versus retained mass 5522. The eight new children +have 16 explicit address maps. The scalar allowance does not include the +full cost of those maps, recursive children, or global precision. Exact +formal scalar prefix bounds have ceiling base-two logarithm 100 for B +and 86 for F; these are not complete recursive precision bounds. + +## Uniqueness and the repair-row bound + +Suppose P has exactly r support rows A and `P=iota_A R_A^-1`. Then +`ker J_offA=im Z`. For the reverse inclusion, let `J_offA v=0` and put +`d=v-ZRv`. We have `Rd=0`, so `Jd=d`. Since JZ is supported on A, d is +also supported there. The unit minor R_A then gives d=0. + +Every source map F with `J_offA F=I_offA` therefore has the unique form +`F=G+ZB`. Since `GP=Z`, this is `G(I+PB)`. It is invertible exactly when +`I+BP` is a unit. If F must also satisfy `LF=R`, then B=0. Thus G is +unique with both this fixed target support and this full logger. +Also `CZ=-P`, so all r correction directions are required. + +For the actual supplier, reduce dyadic coefficients modulo 13. The +identity `RK=14I` gives `RJ=0`, and `RP=I` gives rank R=8. For any source +matrix F, if `C=JF-I`, then `RC=-R`. Thus rank C is at least eight. C +needs at least eight nonzero target rows; their R columns must span the +eight-dimensional query space. The actual A meets this bound. + +This lower bound covers identity-target source preparation followed by +target-row correction. It does not bound arbitrary native circuits or +prove a general minimum number of recursive children. It does not need +F to be invertible. Gaussian dyadics also reduce modulo 13 by mapping +i to 5. For coefficients in the dyadic or Gaussian-dyadic group algebra of +cover permutations, augmentation followed by this reduction gives the +same bound with the stated port support. This extension requires that +augmentation; it does not cover a general algebra of phased native +operators. + +## A conditional query-transport law + +Let charts s and t satisfy the theorem's hypotheses. Let U transport +source fields between them. Suppose their actual selected transport +satisfies `L_t U=V_R L_s`, with its specified mode basis. Since +`R_t G_t^-1=L_t`, + +```text +R_t (G_t^-1 U G_s)=V_R R_s. (2) +``` + +Thus the full query transfers without an inverse of `R_t Z_s`. These +source transitions telescope under compatible ordered composition. +If normalized selected values use `R_T^-1`, their transport V_T gives +`V_R=R_T V_T R_T^-1`; these two matrices must not be identified. + +Equation (2) has an explicit source-transport premise. It does not +restore the full source, close bank bridges, or make the first and last +gauges equal. Also, `G_s^6=I` at each chart does not give order six for a +product of different charts. The portable checker rejects that inference +and a fixed-chart FBF signed-exchange shortcut. + +## Verification and dependencies + +Run the command in [README.md](README.md). The portable entrypoint reads +only immutable Git objects listed in [SOURCES.json](SOURCES.json). The +four earlier examples remain byte-exact and are checked in the same run. +The new words match their independently reviewed literal payloads. The +new checker uses separate propagation from the producer. + +The check covers all 712 formal input columns, arbitrary helper values, +private lifetimes, serial reads, both source inverse orders, exact order +six, scalar counts, typed native access, and all 8192 positive and inverse +Gaussian basis columns for the added recipes. It also checks a noncentral +matrix M and cases with M=0 or M-I=0. These finite cases support, but do +not replace, the ordered proof. + +Negative controls include a missing correction, wrong factor order, +source coding at the wrong cut, an early forward correction, a missing +native line, a positive line at the inverse exit, a wrong scalar phase, +and a missing private clear. [UNIT-TRANSFER-REVIEW.md](UNIT-TRANSFER-REVIEW.md) +states the independent package and literal review scope. + +The historical supplier, source notices, and license are unchanged. +See [NOTICE.md](NOTICE.md) for predecessor credit. This proof, implementation, +and independent agent review used substantial OpenAI Codex assistance +under the user's direction. No independent human review is claimed. diff --git a/research/native-controller-congruence/test_verify.py b/research/native-controller-congruence/test_verify.py new file mode 100644 index 0000000000..d9e98241a3 --- /dev/null +++ b/research/native-controller-congruence/test_verify.py @@ -0,0 +1,398 @@ +#!/usr/bin/env python3 +"""Independent exact tests of the two scoped controller obstructions. + +No producer or predecessor executable is imported. All controller operations +are multiplied as dense rational matrices. The cyclotomic determinant is +extracted only after that multiplication, from the resulting 2 by 2 blocks. +""" + +from fractions import Fraction as Q +from itertools import permutations +from contextlib import contextmanager +import json +from pathlib import Path +import random +import shutil +import subprocess +import sys +import tempfile +import unittest + + +def zero(rows, cols): + return [[Q(0) for _ in range(cols)] for _ in range(rows)] + + +def eye(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def add(a, b, sign=1): + return [[x + sign * y for x, y in zip(ar, br)] + for ar, br in zip(a, b)] + + +def mul(a, b): + return [[sum((x * y for x, y in zip(row, col)), Q(0)) + for col in zip(*b)] for row in a] + + +def inverse(a): + n = len(a) + x = [list(row) + erow for row, erow in zip(a, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if x[i][j]), None) + if pivot is None: + raise ValueError("singular rational matrix") + x[j], x[pivot] = x[pivot], x[j] + scale = x[j][j] + x[j] = [v / scale for v in x[j]] + for i in range(n): + if i != j: + scale = x[i][j] + x[i] = [u - scale * v for u, v in zip(x[i], x[j])] + return [row[n:] for row in x] + + +def rank(a): + x = [list(row) for row in a] + r = 0 + for j in range(len(x[0])): + pivot = next((i for i in range(r, len(x)) if x[i][j]), None) + if pivot is None: + continue + x[r], x[pivot] = x[pivot], x[r] + scale = x[r][j] + x[r] = [v / scale for v in x[r]] + for i in range(r + 1, len(x)): + scale = x[i][j] + x[i] = [u - scale * v for u, v in zip(x[i], x[r])] + r += 1 + return r + + +def block(a, b, c, d): + return [x + y for x, y in zip(a, b)] + [x + y for x, y in zip(c, d)] + + +def determinant(a): + n = len(a) + total = Q(0) + for p in permutations(range(n)): + inversions = sum(p[i] > p[j] for i in range(n) for j in range(i + 1, n)) + value = Q((-1) ** inversions) + for i, j in enumerate(p): + value *= a[i][j] + total += value + return total + + +def cmul(x, y): + """Multiply a+b*t with t^2=t-1, using rational pairs.""" + a, b = x + c, d = y + return (a * c - b * d, a * d + b * c + b * d) + + +def cpower(exponent): + out = (Q(1), Q(0)) + for _ in range(exponent % 6): + out = cmul(out, (Q(0), Q(1))) + return out + + +def cdeterminant(a): + n = len(a) + total = (Q(0), Q(0)) + for p in permutations(range(n)): + inversions = sum(p[i] > p[j] for i in range(n) for j in range(i + 1, n)) + value = (Q((-1) ** inversions), Q(0)) + for i, j in enumerate(p): + value = cmul(value, a[i][j]) + total = tuple(x + y for x, y in zip(total, value)) + return total + + +G = [[Q(1), Q(0), Q(0)], + [Q(0), Q(0), Q(-1)], + [Q(0), Q(1), Q(1)]] + + +def scalar_operation(s): + """A whole-bank scalar operation, repeated on all three sections.""" + banks = len(s) + result = zero(3 * banks, 3 * banks) + for i in range(banks): + for j in range(banks): + for k in range(3): + result[3 * i + k][3 * j + k] = Q(s[i][j]) + return result + + +def macro(banks, first, second, kind, reverse=False): + i3, z3 = eye(3), zero(3, 3) + gi = inverse(G) + local = (block(i3, add(z3, i3, -1), z3, G) if kind == "B" + else block(gi, z3, gi, i3)) + if reverse: + local = inverse(local) + result = eye(3 * banks) + indices = list(range(3 * first, 3 * first + 3)) + list(range(3 * second, 3 * second + 3)) + for i, ri in enumerate(indices): + for j, rj in enumerate(indices): + result[ri][rj] = local[i][j] + charge = (1 if kind == "B" else -1) * (-1 if reverse else 1) + return result, charge + + +def section_determinants(a): + banks = len(a) // 3 + complement = [[a[3 * i][3 * j] for j in range(banks)] for i in range(banks)] + active = [] + for i in range(banks): + row = [] + for j in range(banks): + aa, bb = a[3 * i + 1][3 * j + 1], a[3 * i + 2][3 * j + 1] + if (a[3 * i + 1][3 * j + 2] != -bb + or a[3 * i + 2][3 * j + 2] != aa + bb): + raise ValueError("operation leaves the common-chart commutant") + for u, v in ((0, 1), (0, 2), (1, 0), (2, 0)): + if a[3 * i + u][3 * j + v]: + raise ValueError("operation mixes the fixed and active sections") + row.append((aa, bb)) + active.append(row) + return determinant(complement), cdeterminant(active) + + +def source_chart(r, k, p, ell): + n = len(k) + query = len(r) + if mul(r, p) != eye(query) or mul(ell, k) != eye(query) or mul(ell, p) != zero(query, query): + raise ValueError("chart hypotheses fail") + m = mul(r, k) + z = add(k, mul(p, add(m, eye(query), -1)), -1) + q = add(r, ell, -1) + g = mul(add(eye(n), mul(p, ell), -1), add(eye(n), mul(z, q))) + return g + + +class IndependentControllerTests(unittest.TestCase): + def assert_charge(self, matrix, charge): + fixed, active = section_determinants(matrix) + self.assertNotEqual(fixed, 0) + self.assertEqual(active, tuple(fixed * c for c in cpower(charge))) + + def test_dense_random_interleavings_and_inverses(self): + rng = random.Random(1862) + for banks in (2, 3, 4): + out, charge = eye(3 * banks), 0 + for _ in range(36): + first, second = rng.sample(range(banks), 2) + kind, reverse = rng.choice(("B", "F")), bool(rng.randrange(2)) + op, delta = macro(banks, first, second, kind, reverse) + out, charge = mul(op, out), charge + delta + scalar = eye(banks) + scalar[first][second] = rng.choice((Q(-2), Q(-1, 2), Q(1, 2), Q(1))) + if rng.randrange(2): + scalar[second][second] = -1 + out = mul(scalar_operation(scalar), out) + self.assert_charge(out, charge) + + def test_native_nine_call_charge_and_signs(self): + out, charge = eye(12), 0 + for j, kind in enumerate("FBFBFBFBF"): + op, delta = macro(4, j % 4, (j + 1) % 4, kind) + out, charge = mul(op, out), charge + delta + bridge = eye(4) + bridge[(j + 2) % 4][j % 4] = Q(-1, 2) + out = mul(scalar_operation(bridge), out) + sign = eye(4) + sign[0][0] = -1 + out = mul(scalar_operation(sign), out) + self.assertEqual(charge, -1) + self.assert_charge(out, charge) + fixed, active = section_determinants(out) + self.assertNotEqual(active, (fixed, 0)) + # This is the charge pattern, not a replay of the native controller. + + def test_odd_count_is_obstructed_but_neutral_is_not_sufficient(self): + for charge in range(-15, 16, 2): + self.assertNotEqual(cpower(charge), (1, 0)) + out = eye(6) + op, _ = macro(2, 0, 1, "B") + for _ in range(6): + out = mul(op, out) + self.assert_charge(out, 6) + self.assertNotEqual(out, eye(6)) + self.assertNotEqual(out[0][3], out[1][4]) + + def test_section_dependent_and_noncommuting_controls_rejected(self): + # An uncharged G on one bank would repair the scalar determinant + # ratio. It is outside the scalar-operation alphabet. + out = eye(6) + for i in range(3): + for j in range(3): + out[i][j] = G[i][j] + with self.assertRaises(AssertionError): + self.assert_charge(out, 0) + bad = eye(6) + bad[1][1] = -1 + with self.assertRaises(ValueError): + section_determinants(bad) + bad = eye(6) + bad[0][1] = 1 + with self.assertRaises(ValueError): + section_determinants(bad) + + def test_sign_enabled_two_call_shear_is_allowed(self): + b, _ = macro(2, 0, 1, "B") + sign = scalar_operation([[Q(-1), Q(0)], [Q(0), Q(1)]]) + out = mul(mul(mul(sign, inverse(b)), sign), b) + self.assertEqual(out, scalar_operation([[1, -2], [0, 1]])) + self.assert_charge(out, 0) + + def test_six_call_algebraic_exchange_is_a_positive_control(self): + # Each scaled macro is conjugate by a legal rational whole-bank + # diagonal map. This checks the algebra only: native inverse frame + # progress and the complete physical invoice are separate questions. + b, _ = macro(2, 0, 1, "B") + f, _ = macro(2, 0, 1, "F") + def scale_conjugate(op, first, second): + s = scalar_operation([[Q(first), Q(0)], [Q(0), Q(second)]]) + return mul(s, mul(op, inverse(s))) + b1, b2 = scale_conjugate(b, -1, 1), scale_conjugate(b, -2, 1) + f1, f2 = f, scale_conjugate(f, 1, 2) + upper = mul(inverse(b1), b2) + lower = mul(f1, inverse(f2)) + self.assertEqual(upper, scalar_operation([[1, 1], [0, 1]])) + self.assertEqual(lower, scalar_operation([[1, 0], [-1, 1]])) + out = mul(upper, mul(lower, upper)) + self.assertEqual(out, scalar_operation([[0, 1], [-1, 0]])) + self.assert_charge(out, 0) + + def test_varying_chart_triple_noncentral_and_selected_m(self): + for m in ([[Q(2), Q(1)], [Q(0), Q(3)]], + [[Q(14), Q(0)], [Q(0), Q(14)]]): + i, z = eye(2), zero(2, 2) + r = [ir + zr + zr for ir, zr in zip(i, z)] + k = [list(row) for row in m] + i + z + p0 = i + z + z + l0 = [zr + ir + zr for zr, ir in zip(z, i)] + h = [[Q(0), Q(1)], [Q(-1), Q(0)]] + v = [[Q(1), Q(1)], [Q(0), Q(1)]] + pb = i + z + h + lc = [zr + ir + vr for zr, ir, vr in zip(z, i, v)] + ga = source_chart(r, k, p0, l0) + gb = source_chart(r, k, pb, l0) + gc = source_chart(r, k, p0, lc) + n = len(k) + fa = block(inverse(ga), zero(n, n), inverse(ga), eye(n)) + bb = block(eye(n), add(zero(n, n), eye(n), -1), zero(n, n), gb) + fc = block(inverse(gc), zero(n, n), inverse(gc), eye(n)) + product = mul(fc, mul(bb, fa)) + expected_defect = add(gb, inverse(gc), -1) + self.assertEqual(product, block(zero(n, n), add(zero(n, n), inverse(gc), -1), + mul(gb, inverse(ga)), expected_defect)) + self.assertEqual(mul(r, mul(expected_defect, k)), add(m, [[2, 0], [0, 2]], -1)) + self.assertGreaterEqual(rank(expected_defect), rank(add(m, [[2, 0], [0, 2]], -1))) + # Arbitrary invertible endpoint gauges cannot erase this block. + left, right = eye(n), eye(n) + left[0][1], right[2][3] = Q(1, 2), Q(-2) + self.assertEqual(rank(mul(left, mul(expected_defect, right))), rank(expected_defect)) + + def test_each_chart_hypothesis_is_checked(self): + r, k = [[Q(1), Q(0), Q(0)]], [[Q(14)], [Q(1)], [Q(0)]] + p, ell = [[Q(1)], [Q(0)], [Q(0)]], [[Q(0), Q(1), Q(0)]] + source_chart(r, k, p, ell) + for rr, kk, pp, ll in ( + (r, k, [[Q(2)], [Q(0)], [Q(0)]], ell), + (r, [[Q(14)], [Q(2)], [Q(0)]], p, ell), + (r, k, [[Q(1)], [Q(1)], [Q(0)]], ell), + ): + with self.assertRaises(ValueError): + source_chart(rr, kk, pp, ll) + + def test_selected_query_rank_eight_projection(self): + # A fresh canonical realization of RK=14I, not the pinned source + # matrices: the producer separately binds the actual 112-port data. + i, z = eye(8), zero(8, 8) + m = [[14 * x for x in row] for row in i] + r = [ir + zr + zr for ir, zr in zip(i, z)] + k = m + i + z + p = i + z + z + ell = [zr + ir + zr for zr, ir in zip(z, i)] + g = source_chart(r, k, p, ell) + defect = add(g, inverse(g), -1) + projection = mul(r, mul(defect, k)) + self.assertEqual(projection, [[12 * x for x in row] for row in i]) + self.assertEqual(rank(projection), 8) + self.assertGreaterEqual(rank(defect), 8) + + +class ReplayIntegrityTests(unittest.TestCase): + """Exercise the CLI trust boundary in disposable copies, never --write.""" + + @contextmanager + def isolated_package(self): + source = Path(__file__).resolve().parent + root = source.parents[1] + pins = json.loads((source / "ARCHIVE.json").read_text()) + predecessor = json.loads((source / "PREDECESSOR.json").read_text()) + with tempfile.TemporaryDirectory(prefix="native-controller-integrity-") as tmp: + tmp_root = Path(tmp) + package = tmp_root / "research" / source.name + package.mkdir(parents=True) + local_files = ["verify.py", "ARCHIVE.json", "PREDECESSOR.json", "RESULT.json"] + local_files += [item["local_path"] for item in predecessor["sources"]] + for name in local_files: + target = package / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(source / name, target) + archive = tmp_root / pins["path"] + archive.parent.mkdir(parents=True, exist_ok=True) + archive.symlink_to(root / pins["path"]) + yield package + + def replay(self, package): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=package, capture_output=True, text=True, + timeout=120, check=False) + + def test_entrypoint_positive_and_corrupted_result_controls(self): + with self.isolated_package() as package: + clean = self.replay(package) + self.assertEqual(clean.returncode, 0, clean.stderr) + result = json.loads(clean.stdout) + self.assertEqual(result["status"], "PASS_NATIVE_CONTROLLER_CONGRUENCE") + result["signed_winding"] = 0 + (package / "RESULT.json").write_text(json.dumps(result)) + corrupted = self.replay(package) + self.assertNotEqual(corrupted.returncode, 0) + self.assertIn("recorded result mismatch", corrupted.stderr) + (package / "RESULT.json").write_text("{broken-json") + malformed = self.replay(package) + self.assertNotEqual(malformed.returncode, 0) + self.assertIn("JSONDecodeError", malformed.stderr) + + def test_archive_binding_control(self): + with self.isolated_package() as package: + pins_path = package / "ARCHIVE.json" + pins = json.loads(pins_path.read_text()) + pins["sha256"] = "0" * 64 + pins_path.write_text(json.dumps(pins)) + corrupted = self.replay(package) + self.assertNotEqual(corrupted.returncode, 0) + self.assertIn("archive pin", corrupted.stderr) + + def test_predecessor_text_binding_control(self): + with self.isolated_package() as package: + predecessor = json.loads((package / "PREDECESSOR.json").read_text()) + text = package / predecessor["sources"][0]["local_path"] + text.write_bytes(text.read_bytes() + b"\nChanged claim, same alleged source.\n") + corrupted = self.replay(package) + self.assertNotEqual(corrupted.returncode, 0) + self.assertIn("predecessor text pin", corrupted.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/native-controller-congruence/verify.py b/research/native-controller-congruence/verify.py new file mode 100644 index 0000000000..ea2936c500 --- /dev/null +++ b/research/native-controller-congruence/verify.py @@ -0,0 +1,213 @@ +"""Exact selected-source binding; independent of predecessor executables. + +Apache-2.0. Prepared with substantial OpenAI Codex assistance. +""" +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import gzip +import json +import sys +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ident(n): + return [{i: F(1)} for i in range(n)] + + +def plus(a, b, scale=1): + require(len(a) == len(b), "row count mismatch") + out = [row.copy() for row in a] + for dst, src in zip(out, b): + for j, x in src.items(): + v = dst.get(j, F(0)) + scale*x + if v: + dst[j] = v + else: + dst.pop(j, None) + return out + + +def mul(a, b): + out = [] + for row in a: + dst = {} + for k, x in row.items(): + for j, y in b[k].items(): + dst[j] = dst.get(j, F(0)) + x*y + out.append({j: x for j, x in dst.items() if x}) + return out + + +def chart(R, K, P, L): + r, n = len(R), len(K) + require(mul(R, P) == ident(r), "RP is not identity") + require(mul(L, K) == ident(r), "LK is not identity") + require(not any(mul(L, P)), "LP is not zero") + M = mul(R, K) + Q = plus(R, L, -1) + Z = plus(K, mul(P, plus(M, ident(r), -1)), -1) + G = plus(plus(ident(n), mul(Z, Q)), mul(P, R), -1) + Gi = plus(plus(ident(n), mul(P, L)), mul(Z, R), -1) + require(mul(Q, P) == mul(L, Z) == ident(r), "section left inverses") + require(not any(mul(Q, Z)), "sections not disjoint") + require(mul(G, P) == Z and mul(G, Z) == plus(Z, P, -1), "active action") + require(mul(Gi, P) == plus(P, Z, -1) and mul(Gi, Z) == P, "active inverse") + require(mul(R, G) == Q and mul(R, Gi) == L, "query action") + projection = plus(mul(P, Q), mul(Z, L)) + W = plus(ident(n), projection, -1) + require(mul(G, W) == W and mul(Gi, W) == W, "fixed complement") + require(mul(projection, projection) == projection, "not a projection") + require(sum(projection[i].get(i, 0) for i in range(n)) == 2*r, "section rank") + return {"G": G, "inverse": Gi, "M": M, "P": P, "L": L, + "fixed_dimension": n-2*r} + + +def sources(): + pins = json.loads((HERE / "ARCHIVE.json").read_text()) + path = ROOT / pins["path"] + require(sha256(path.read_bytes()).hexdigest() == pins["sha256"], "archive pin") + out = {} + with tarfile.open(path, "r:gz") as archive: + for name, pin in pins["members"].items(): + entries = [m for m in archive.getmembers() if m.name == name] + require(len(entries) == 1 and entries[0].isfile(), "ambiguous archive member") + raw = archive.extractfile(entries[0]).read() + require(sha256(raw).hexdigest() == pin["sha256"], "member pin") + raw = gzip.decompress(raw) + require(sha256(raw).hexdigest() == pin["payload_sha256"], "payload pin") + out[Path(name).name] = json.loads(raw) + predecessor = json.loads((HERE / "PREDECESSOR.json").read_text()) + for item in predecessor["sources"]: + require(sha256((HERE/item["local_path"]).read_bytes()).hexdigest() + == item["sha256"], "predecessor text pin") + return out + + +def extract_query(word, program): + """Replay source columns only; helper/private outputs are not audited.""" + v = word["v"] + n = 2*v + word["R"] + require((v, n, word["h"]) == (112, 704, 9), "supplier dimensions") + rows = ident(v) + [{} for _ in range(n+8-v)] + cut = ["phase", "centers"] + require(program.count(cut) == 1, "ambiguous centre cut") + for event in program[:program.index(cut)]: + if event[0] != "scalar": + continue + op = event[1] + def at(port): + require(port[0] in ("C", "L"), "unknown field") + return port[1] + (n if port[0] == "C" else 0) + dst = at(op[1]) + if op[0] == "clear": + rows[dst] = {} + elif op[0] == "copy": + rows[dst] = rows[at(op[2])].copy() + elif op[0] == "scale": + c = F(op[2], op[3]) + rows[dst] = {j: c*x for j, x in rows[dst].items() if c*x} + else: + require(op[0] == "add", "unknown scalar operation") + rows[dst] = plus([rows[dst]], [rows[at(op[2])]], F(op[3], op[4]))[0] + R = [rows[c] for c in word["centers"]] + require(len(R) == 8, "query dimension") + return R + + +def cyclo_mul(x, y): + # Q[t]/(t^2-t+1), represented by a+b*t. + a, b = x + c, d = y + return (a*c-b*d, a*d+b*c+b*d) + + +def cyclo_power(k): + t = (0, 1) if k >= 0 else (1, -1) + out = (1, 0) + for _ in range(abs(k)): + out = cyclo_mul(out, t) + return out + + +def winding(operations): + tariff = {"B": 1, "F": -1, "B_inverse": -1, "F_inverse": 1} + require(all(x in tariff for x in operations), "unknown macro") + return sum(tariff[x] for x in operations) + + +def run(): + data = sources() + R = extract_query(data["CANONICAL-WORD.json.gz"], data["LOCAL-PROGRAMS.json.gz"]["forward"]) + K = [{k: R[k][p]/4 for k in range(8) if p in R[k]} for p in range(112)] + A = [0, 7, 20, 27, 36, 46, 57, 111] + T = [21, 37, 47, 76, 81, 87, 92, 110] + def make(a, t): + P = [row.copy() if p in a else {} for p, row in enumerate(K)] + L = [{p: c for p, c in row.items() if p in t} for row in R] + return chart(R, K, P, L) + base, alternate = make(A, T), make(T, A) + require(base["M"] == [{k: F(14)} for k in range(8)], "RK is not 14I") + require(base["fixed_dimension"] == 96, "fixed complement dimension") + for b in (base, alternate): + for c in (base, alternate): + defect = mul(mul(R, plus(b["G"], c["inverse"], -1)), K) + require(defect == [{k: F(12)} for k in range(8)], "three-call rank witness") + locals_ = [x for x in data["GLOBAL-TEMPLATE.json.gz"]["recipe"] if x["kind"] == "local"] + require([(x["pair"], x["reverse"], x["stage"]) for x in locals_] == [ + (0, False, 0), (0, True, 1), (0, False, 2), + (1, True, 3), (1, False, 4), (2, True, 5), + (2, False, 6), (3, True, 7), (3, False, 8)], "four-pair nine-stage recipe") + sequence = ["B" if x["reverse"] else "F" for x in locals_] + require(Counter(sequence) == {"B": 4, "F": 5}, "orientation count") + require(winding(sequence) == -1, "selected signed winding") + residues = [list(cyclo_power(k)) for k in range(6)] + require(len(set(map(tuple, residues))) == 6 and cyclo_power(6) == (1, 0), "exact order six") + for k in range(-60, 61): + require((cyclo_power(k) == (1, 0)) == (k % 6 == 0), "congruence control") + require(cyclo_power(winding(sequence)) != (1, 0), "nine-stage obstruction lost") + require(winding(["B", "B_inverse"]) == winding(["B", "F"]) == 0, "inverse sign control") + require(cyclo_power(3) == (-1, 0), "third power must not be called identity") + # An active-sector-only determinant could incorrectly cancel this -1. + require((-1)*cyclo_power(3)[0] == 1 and -1 != 1, "missing-complement control") + badP = [row.copy() for row in base["P"]] + badP[A[0]] = {} + try: + chart(R, K, badP, base["L"]) + except ValueError: + pass + else: + raise ValueError("broken selected minor accepted") + serial = [[str(row.get(j, 0)) for j in range(112)] for row in R] + return { + "status": "PASS_NATIVE_CONTROLLER_CONGRUENCE", + "selected_source_query_sha256": sha256(json.dumps(serial, separators=(",", ":")).encode()).hexdigest(), + "ports": 112, "query_rank": 8, "fixed_dimension": 96, + "minimal_polynomial_low_to_high": [-1, 2, -2, 1], + "active_powers_0_to_5": residues, "recipe": sequence, "signed_winding": -1, + "required_winding_modulus": 6, "changed_chart_pairs_checked": 4, + "changed_chart_defect_compression": "12 I_8", + "changed_chart_defect_rank_lower_bound": 8, + "selected_frontier_changed": False, + "coverage": "Source-column prefix and scalar-controller algebra; no native or all-size cold replay." + } + + +if __name__ == "__main__": + result = run() + raw = json.dumps(result, indent=2) + "\n" + if sys.argv[1:] == ["--write"]: + (HERE / "RESULT.json").write_text(raw) + else: + require(not sys.argv[1:], "unknown option") + require(json.loads((HERE / "RESULT.json").read_text()) == result, "recorded result mismatch") + print(raw, end="") From 165f08a694b26b0f4c521ce5e1132ede0b7362a2 Mon Sep 17 00:00:00 2001 From: David Arias Date: Wed, 14 Oct 2026 10:41:04 -0500 Subject: [PATCH 2/2] Link predecessor PRs and name their authors --- .../native-controller-congruence/README.md | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/research/native-controller-congruence/README.md b/research/native-controller-congruence/README.md index a8e7abf699..e2ca6a83df 100644 --- a/research/native-controller-congruence/README.md +++ b/research/native-controller-congruence/README.md @@ -1,13 +1,13 @@ # A determinant obstruction for native source-code controllers -**Scoped structural result; no new supplier or kappa.** PR1862 supplies exact +**Scoped structural result; no new supplier or kappa.** Ali Romman’s [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) supplies exact local identity transfers that store an eight-coordinate centre query in existing data fields. Its remaining obstacle is a complete controller that removes the source code while delivering the required data endpoint. This package rules out an unbounded class of proposed controllers, rather than searching words only up to a length cutoff. -For one fixed source code, every completed controller built from PR1862's +For one fixed source code, every completed controller built from [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862)'s forward/backward transfers, their inverses, and arbitrary invertible scalar mixing of whole port banks must have **signed code winding divisible by six**. The statement allows any number of data banks and restored dirty auxiliary @@ -26,12 +26,12 @@ These are controller-interface obstructions. Port-dependent scalar maps, physical changes of chart, new clean workspace, and paid repairs remain outside the first theorem. The second theorem does not include interleaved bank mixing or arbitrary native chart transports. Neither result is a lower -bound for all multiplication algorithms or a rejection of PR1862's valid +bound for all multiplication algorithms or a rejection of [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862)'s valid local construction. ## The pinned local interface -Write a port bank as an n-vector. PR1862 works over the dyadic coefficient +Write a port bank as an n-vector. [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) works over the dyadic coefficient ring with maps R of size r by n, K of size n by r, and maps P,L satisfying ```text @@ -74,7 +74,7 @@ f(t) = (t-1)(t^2-t+1), not just a polynomial that happens to annihilate G. Both summands are nonzero, and the two factors are coprime. In particular, the algebra Q[G] is faithfully represented by `A = Q[t]/(f)` and t has order exactly six. -The local construction and these identities retain PR1862's attribution. +The local construction and these identities retain [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862)'s attribution. ## Theorem 1: balance for every word in one fixed chart @@ -158,7 +158,7 @@ The retained four-pair construction starts with F_0 and then uses exchange. It therefore contains four B calls and five F calls. Bridges and the signed exchange are scalar whole-bank maps; they cannot change w=-1. -Substituting one fixed PR1862 source code into this skeleton cannot give its +Substituting one fixed [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) source code into this skeleton cannot give its required scalar identity, regardless of how its scalar whole-bank controller is redesigned. This covers all whole-bank scalar repairs at the same nine macro calls, not only the displayed bridge constants. More generally, no @@ -233,9 +233,9 @@ The predecessor proof and notice are exact text copies under `references/`, with their original relative links referring to the pinned upstream package. No predecessor executable is imported. -The source-bound verifier reads three pinned members of the selected PR1094 +The source-bound verifier reads three pinned members of the selected [PR #1094](https://github.com/CrocSwap/integer-mult-bounds/pull/1094) replay archive. Its local word and program payloads are byte-identical to the -PR1042 inputs consumed by PR1862. It replays the **112 source columns only** +[PR #1042](https://github.com/CrocSwap/integer-mult-bounds/pull/1042) inputs consumed by [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862). It replays the **112 source columns only** up to the forward centre cut, derives R,K,P,L and the 96+16 decomposition, and checks `RDK=12I_8` for all four pairs of the actual A/T and swapped T/A charts. The retained parent `GLOBAL-TEMPLATE` supplies only the exact @@ -270,7 +270,7 @@ unchanged. six, followed by a typed native-frame replay and full child profile. The blocker is useful coordinate progress: cancellation by a true inverse can erase the very transformation the supplier needs to perform. -- **A priced escape through actual chart transport.** PR1862's law +- **A priced escape through actual chart transport.** [PR #1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862)'s law `R_t(G_t^-1 U G_s)=V_R R_s` is conditional on the selected transport. Derive one actual stage transition, including its port-dependent address maps, and check full-source restoration as well as query transport. @@ -304,8 +304,10 @@ inside the excluded odd-call class can remove its determinant obstruction. reproving its source-support or native-frame statement. - The retained four-pair scalar chain and native geometry come from the split-centres/gauge44 construction and its inherited authors. The pinned - PR1042/PR1094 lineage retains Jeremy Kothe, Chafik Boukhalfa, Rohan Arun, - Hao Yan, icekylinx, NewBArch and the source-specific notices. No historical + source lineage includes Jeremy Kothe’s [PR #1042](https://github.com/CrocSwap/integer-mult-bounds/pull/1042) + and Rohan Arun’s [PR #1094](https://github.com/CrocSwap/integer-mult-bounds/pull/1094), + with Chafik Boukhalfa, Hao Yan, icekylinx, NewBArch and the source-specific + notices retaining their attribution. No historical construction or selected evidence is modified. Prepared by David Arias with substantial OpenAI Codex assistance in scoping,