From 65445e68d79d7e9f289d4f97e0aa4a8416f2438f Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Fri, 23 Oct 2026 00:52:46 -0700 Subject: [PATCH] Prove and cost one physical inverse-coded FULL/thin pair --- research/physical-inverse-pair/README.md | 94 ++++++++++ research/physical-inverse-pair/RESULT.json | 74 ++++++++ research/physical-inverse-pair/SOURCES.json | 54 ++++++ research/physical-inverse-pair/TASK.json | 97 +++++++++++ research/physical-inverse-pair/VERIFY.json | 37 ++++ research/physical-inverse-pair/verify.py | 184 ++++++++++++++++++++ 6 files changed, 540 insertions(+) create mode 100644 research/physical-inverse-pair/README.md create mode 100644 research/physical-inverse-pair/RESULT.json create mode 100644 research/physical-inverse-pair/SOURCES.json create mode 100644 research/physical-inverse-pair/TASK.json create mode 100644 research/physical-inverse-pair/VERIFY.json create mode 100644 research/physical-inverse-pair/verify.py diff --git a/research/physical-inverse-pair/README.md b/research/physical-inverse-pair/README.md new file mode 100644 index 0000000000..a4ed4756ea --- /dev/null +++ b/research/physical-inverse-pair/README.md @@ -0,0 +1,94 @@ +# One physical inverse-coded FULL/thin pair + +**Scoped exact all-block identity with a charged local recipe; no new kappa or complete caller admission.** Replacing the scalar inverse in PR5036 by the physical inverse does repair one backward FULL / next thin pair, provided its Y entrance and Y exit are also changed. The exit is a real operation: the explicit implementation adds 224 rank-one Gaussian jobs beyond the thin stage's 112. It is not a free gauge. + +The exact sources are pinned in [SOURCES.json](SOURCES.json), at canonical base `4c0a359d88f22f05189d51f48387750b801a45d4`, priority revision 7. The assigned claim is [Discussion #4930](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19140791). The pair is stages 37/38 of the proposed p19 chronology; no bridge or initial IDLE separates those calls. This package changes the operator and boundary left open by PR5036, rather than repeating its scalar counterexample. It excludes the separately claimed two-stage terminal-code product and all full-controller work. + +## Literal four-block theorem + +Operators act rightmost first. On the direct sum of 112 arbitrary owner fields let `Q` be the central Gaussian, `D` the product of the eight fresh Gaussian axes, `R=DQ=QD`, and `K=diag(K_i)` the actual PR4933 signed normalizers. Set + +```text +C = K^-1 (A tensor I) K, +B = diag(D,D) [[I,-QC],[0,I]], +T = [[I,0],[Q^-1 C^-1,I]], +E = diag(I,C^-1), O = diag(I,Q^-1 C Q). +``` + +The raw-dual convention is PR4933's actual X-only Q-squared correction. Each real signed K_i commutes with R, hence C and its inverse commute with R. Consequently literal multiplication gives every block, without commuting C through Q or D separately: + +```text +T B = [[D, -DQ C], + [Q^-1 C^-1 D, 0]], + +O T B E = [[D, -DQ], + [DQ^-1, 0]]. +``` + +For the bottom-right block use `Q^-1 C^-1 DQ C = Q^-1 DQ = D`. For the top-right block right-multiplication by C^-1 cancels the final C. For the bottom-left block left-multiplication by `Q^-1 C Q` cancels adjacent `Q Q^-1` and `C C^-1`, giving `Q^-1 D=DQ^-1`. The top-left block stays D. These equations hold on independent arbitrary X and Y, not only on x=0 or a selected source column. The uncorrected pair already cancels its YY block; its YX block is still wrong. A scalar exit C, with the Q conjugation omitted, fails the executable control. + +The inherited producer's complete direct-sum endpoint includes 408 autonomous helper operators. E, T's new work and O address only main/query/mode banks. Extend each by identity on the helpers and every unrelated spectator. Block multiplication therefore retains exactly those 408 original independent outputs, with their original requested transforms; it does not identify them with scratch or with unchanged input values. Their physical producer autonomy is the pinned PR4929 premise, not a new native replay here. + +## Source signs and every positive width + +For one nine-bit column write `K_i=Z_(z_i) P_(G_i)`. On the Walsh character `chi_u(x)=(-1)^(u dot x)`, its inverse maps the frequency to `G_i^T(u xor z_i)`. The Gaussian Q has eigenvalue `i^(u_0)` and R has eigenvalue `i^wt(u)`. The checker independently reads the actual G and z, verifies orthogonality and the actual central port, then checks + +```text +wt(G_i^T(u xor z_i)) = wt(u) (mod 4) +``` + +for all 112 owners and all 512 frequencies. This is a complete finite certificate for the actual one-column absolute-phase commutator, not a supplied commutator hypothesis. Omitting the signed Z masks fails. PR4933's written orthogonal weight-congruence derivation supplies the same identity in address coordinates. + +For every positive column count f, take `K_i,f=K_i^tensor f`, `Q_f=Q^tensor f` and `D_f=D^tensor f`, with all other coordinates as spectators. The one-column equality tensors, so `[K_i,f,D_f Q_f]=0`. Define `C_f` by its owner entries `A_ij K_i,f^-1 K_j,f`; apply A once across owners, not once per digit column. The scalar program's inverse follows from the exact source relations `A=I-MM^T/4`, `M^T M=56I`, and `A^-1=I-MM^T/52`. Thus the displayed four-block calculation evaluates in the lifted operator algebra for every f. No tensor-of-a-sum substitution occurs. + +For independent finite corroboration, a common Walsh frequency tuple defines an invariant 112-owner subspace with physical frequency `v_i=(G_i^T(u_t xor z_i))_t` at owner i. In this chart C is A, while Q and D are genuinely owner-dependent diagonal phases, `q_i=i^(sum_t(v_i,t)_0)` and `d_i=i^(sum_t wt(v_i,t>>1))`. The interpreter executes entrance, backward FULL, changed thin and exit in chronological order and compares with the independent standard-pair endpoint. It tests all 224 X/Y basis columns in eight explicitly recorded width1/2 subspaces, plus mixed inputs. This finite oracle does not enumerate every width-two physical address; the quantified coverage is the preceding tensor/operator proof. All 512 Walsh coefficients of the required physical input x=0, y=owner1/address1 are separately checked. The source witness `C_01|1>=+|22>/2`, versus scalar `A_01|1>=-|1>/2`, still rejects the old scalar recipe. + +## Constructive local instruction schedule and complete ledger + +The exact rational field program is: (1) on Y apply K, inverse scalar mode code, K^-1; (2) invoke the source backward FULL with its actual normalization; (3) initialize 112 owned query fields, copy X, recode those fields by physical C^-1, apply Q^-1 to each, ADD each result to its distinct Y owner, and erase only those owned query fields; (4) on Y apply Q, physical C, then Q^-1. The query buffers can be released before the exit. Each scalar code first collects all eight modes before overwriting any owner. Its mode workspace is reused across the three recodings. Native helpers are never available as borrowed work. + +A Q^-1 job is lowered as one positive rank-one Gaussian Q and its Pauli translation Q^-2; it is not treated as an order-two Gaussian. The source all-column query/job ABI and its internal scratch remain inherited. Exit Q and Q^-1 act on the current Y bank, preserving X; they receive no main-output rank credit. A source job's in-place realization and movement must satisfy that ABI and are not supplied by the linear identity alone. + +| Operation | Explicit local charge | Evidence/status | +| --- | ---: | --- | +| Backward center-free FULL | `2201 H1 + 412 H2 + 510 H3 + 127 H4 + 40 H5` | Inherited source profile | +| Original autonomous helper returns | `28 H4 + 7 H7 + 47 H8 + 326 H9` | 408 distinct owners, no scratch or erasure credit | +| Actual four port wrappers | 448 monomial field maps | Inherited constructive bound | +| X-only backward conversion | At most 448 monomial maps | Inherited bound, no fusion assumed | +| Entrance physical C^-1 | 224 K maps, 896 ADDs, 16 owned CLEARs | Exact eight-mode program, coefficient -1/52 | +| Thin physical C^-1 | 224 K maps, 896 ADDs, 16 owned CLEARs | Same program on owned query copies | +| Exit physical C | 224 K maps, 896 ADDs, 16 owned CLEARs | Eight-mode program, coefficient -1/4 | +| Thin owned query bank | 112 initial CLEARs, 112 COPYs, 112 terminal ERASEs | Only owned query fields | +| Thin Q^-1 plus destination update | 112 H1, 112 Pauli maps, 112 ADDs | Positive Gaussian lowering | +| Exit Q then Q^-1 | 224 H1, 112 Pauli maps | Q conjugation is explicitly paid | + +The complete paid Gaussian profile of this emitted recipe is `{1:2537,2:412,3:510,4:127,5:40}`. It includes 336 added H1 jobs, not merely 112. Its additional explicit scalar ADD count is 2,800 (2,688 recoding ADDs plus 112 destination updates), and the wrapper/query monomial upper bound is 1,792 (448+448+672+224), beyond the native internal word. There are 48 mode CLEARs, 112 query CLEARs, 112 COPYs and 112 terminal ERASEs. Additional field workspace peaks at 120 owned fields: 112 query copies plus eight modes, beyond source native/query internal scratch. These are constructive field-operation upper bounds, not a compiled physical tape tariff or a claim of optimality. Fusion or amortization would need a separately priced replacement word. + +Both inverse recodings introduce denominator 13; exit C is dyadic. For N real/imaginary scalar components per owner, the retained PR5037 classical grid kernel implements one scalar inverse within `2*2^-P` component error and charges `N(2898W+5922)+18W+100` transitions, with `W=bit_length(56H+2)+1` for a validated input bound H. Conditional on that kernel's common-coordinate, classical-overwrite ABI, the two calls cost the sum of that expression at their respective H/N values, with all 224 K maps per invocation additional. Its nine word buffers represent the eight modes plus one reusable division buffer at the current scalar coordinate; that additional division word and its scans are already included in the kernel tariff, not counted as nine extra field owners. It cannot be substituted into the exact identity as an exact inverse, and its output error requires propagation through the actual Gaussian/interstage suffix. The kernel is noninjective and does not provide reversible cleanup. + +The exact field program has finite local norm bounds: source inverse mode prefixes at most 56 and forward prefixes at most 57; signed K preserves component magnitude. A fixed finite composition of these and actual Gaussian operators yields a finite error-propagation constant. Selecting a global precision and funding that constant is still a caller obligation. Native ordinary arithmetic (including the retained 6,596 dyadic compensation ADDs), matching, routing, field movement, query-internal work, denominator rounding, and compiler/outer error funding remain inherited or explicitly unknown nonzero costs. There is no claimed complete bit/tape invoice for the physical composition. + +## Family decision and remaining obligations + +**Finish this local implication; do not expand the p19 construction from it.** The algebraic missing implication is resolved for this changed recipe. The honest recipe has 224 extra boundary H1 jobs compared with the already-charged thin-only alternative, and no evidence here makes those free. Its complete field inventory is known; physical tariff and full-controller affordability are not. A downstream expansion must present a named complete caller allowance and legal interstage boundary composition, or a different explicit costed decoder. A favorable local cancellation is insufficient. The selected conditional kappa `0.00302015` is unchanged. + +## Reproduce and validation scope + +```sh +python3.12 -I -B research/physical-inverse-pair/verify.py +python3.12 -I -O -B research/physical-inverse-pair/verify.py +python3.12 -B scripts/research_package.py --package research/physical-inverse-pair +``` + +The standard-library verifier authenticates every live source input, checks every code entry and the mode Gram matrix, actual signed phases, independent basis/mixed inputs, and the literal physical address fixture. Semantic controls reject an omitted entry recoding, an unconjugated exit, reversed thin operator order, omitted K signs, the old scalar substitution and an attempt to erase helper 17. Assertions are not used for correctness. The all-width proof, source-bound finite certificate, and conditional implementation ledger are different claims. No full native/controller replay, Lean, Docker, production build, physical TM execution, or complete multiplication theorem is claimed. + +Test-authoring rationale: the observable contract is the chronological all-block physical pair; plausible regressions are the six listed semantic mutations; predecessors do not test the changed C^-1 recipe with its new Y boundaries; the checker adds no production-only API or test seam. + +## Open next questions + +1. Can a complete caller afford these boundaries, or can a concrete shared boundary word remove their paid queries? First compare this full field inventory with a named allowance; stop if the optimistic complete bill fails. No two-stage terminal-code product analysis is supplied here. +2. Can the caller realize the stated common-coordinate field accesses, classical cleanup and finite-precision inverses with a complete physical tariff? Start with one actual boundary and its numerical range; the scalar PR5037 kernel alone does not resolve Gaussian propagation or reversible ownership requirements. + +## Credit + +Cayden Burkart / SethBurkart123 supplies PR4940's coded reverse chronology; Dillon supplies PR4933's actual signed normalizers, physical ABI, mode factorization and local bounds; Dugongue / mdumitrean supplies PR4929's coded producer. Credit Cinna Davis for PR4440/4470/4694/4698, Cao Yifan / intqwq, zxv, Jacob Alan Sussman, and all retained native, Clifford, query, ownership, precision and compiler contributors. JoyboyBrian's PR5036 scalar gap and PR5037 finite-grid kernel are retained predecessors. The new result is the one-pair all-block correction and honest boundary-inclusive ledger. Prepared for JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. Independent human or formal-kernel acceptance is not claimed. diff --git a/research/physical-inverse-pair/RESULT.json b/research/physical-inverse-pair/RESULT.json new file mode 100644 index 0000000000..e0a81e0275 --- /dev/null +++ b/research/physical-inverse-pair/RESULT.json @@ -0,0 +1,74 @@ +{ + "status": "PASS_PHYSICAL_INVERSE_PAIR", + "scope": "One-stage exact operator identity; conditional physical ledger, no new kappa", + "normalizer_absolute_phase_checks": 57344, + "widths": [ + 1, + 2 + ], + "walsh_fibers": [ + [ + 0 + ], + [ + 1 + ], + [ + 19 + ], + [ + 511 + ], + [ + 0, + 1 + ], + [ + 1, + 19 + ], + [ + 17, + 256 + ], + [ + 511, + 511 + ] + ], + "independent_main_basis_columns": 1792, + "physical_address1_walsh_coefficients": 512, + "mixed_input_checks": 8, + "helpers": "408 inherited autonomous output operators; never scratch", + "semantic_rejections": [ + "omit_exit_q", + "omit_entry", + "wrong_order", + "unsigned_K", + "old_scalar_A", + "helper_erasure" + ], + "added_paid_rank1_jobs": 336, + "total_paid_profile": { + "1": 2537, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "wrapper_monomial_maps_upper": 1792, + "scalar_adds": 2800, + "recoding_owned_clears": 48, + "query_initial_clears": 112, + "query_copies": 112, + "query_owned_erases": 112, + "recoding_field_workspace": 120, + "inverse_recode_calls": 2, + "forward_recode_calls": 1, + "unknown_nonzero_costs": [ + "Native/query internal scratch and movement", + "Physical field-map and rational ADD tape tariffs", + "Finite precision and global error budget", + "Full-controller bridge and boundary accounting" + ] +} diff --git a/research/physical-inverse-pair/SOURCES.json b/research/physical-inverse-pair/SOURCES.json new file mode 100644 index 0000000000..3158ec24cc --- /dev/null +++ b/research/physical-inverse-pair/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coded-inverse-fixed-grid/PROOF.md", + "usage": "input", + "git_blob": "a465ed5ce6b0bd7ac03bc79e72003380a839d7f4", + "sha256": "2bf523cf4f4b3e6bd90805e86f2cbf5d1d85142c16e751e72f09480bcdbee5cd" + }, + { + "path": "research/coded-native-caller/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/coded-native-caller/PHYSICAL.md", + "usage": "input", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + { + "path": "research/coded-reverse-controller/verify.py", + "usage": "input", + "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c", + "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67" + }, + { + "path": "research/coded-reverse-physical-pair-gap/README.md", + "usage": "input", + "git_blob": "fe31036c0ee2f35583767ee32dc0160e0aeb4f72", + "sha256": "cc258ef038af79dfcda1be97156cf2164f936a38ebf8e06ddf186ea8be56fae9" + } + ] +} diff --git a/research/physical-inverse-pair/TASK.json b/research/physical-inverse-pair/TASK.json new file mode 100644 index 0000000000..4670801a58 --- /dev/null +++ b/research/physical-inverse-pair/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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": [ + "docs/research/research-family-status.md", + "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=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/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.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "One physical backward FULL / changed thin pair with all-block entrance/exit correction and full local operation ledger; no two-stage product or full controller.", + "scope_change_reason": "PR5036 leaves the explicitly handed-off physical C^-1 thin recipe and its boundary unresolved. Replace the operator rather than repeat the scalar failure.", + "bottleneck_link": "Deleting the center paths only helps if the changed physical consumer and its boundary realize the claimed uncoded jobs within a complete budget.", + "budget_minutes": 60, + "stop_rule": "Stop at this local identity and complete field-operation ledger with unknown physical tariffs explicit; no family expansion or p19 replay.", + "outcome": "partial", + "evidence": "Proved O T B E = standard pair at every positive width. Source-bound signed phase certificate and bounded width1/2 all-owner oracle pass; explicit complete field ledger adds 336 H1 jobs. Physical tape/precision and full-controller funding remain open.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, operator derivation, implementation and checks.", + "open_questions": [ + { + "question": "Can a complete caller afford or remove these explicitly charged one-pair boundaries?", + "why_it_matters": "The local equality adds positive Gaussian work and cannot import the scalar p19 invoice.", + "first_step": "Compare the complete boundary-inclusive paid profile against a named caller allowance before any expansion.", + "blocked_by": "No complete caller budget or legal interstage amortization is supplied." + } + ], + "first_fixture": { + "x": 0, + "y": "owner1,address1", + "widths": [ + 1, + 2 + ], + "pair": [ + 37, + 38 + ], + "p": 19 + }, + "success_condition": "Prove every block on arbitrary independent X,Y and preserve 408 autonomous helper jobs; explicitly price entrance C^-1, thin C^-1 and exit Q^-1 C Q.", + "bounds": { + "owners": 112, + "modes": 8, + "address_bits_per_column": 9, + "widths": [ + 1, + 2 + ], + "max_oracle_seconds": 10 + }, + "inherited_obligations": [ + "PR4929 arbitrary-input native ABI and 408 autonomous jobs", + "PR4933 actual signed monomial wrappers", + "PR4440 positive Gaussian query and owned erasure ABI", + "Physical movement, precision allocation, denominator rounding and global compiler admission" + ] +} diff --git a/research/physical-inverse-pair/VERIFY.json b/research/physical-inverse-pair/VERIFY.json new file mode 100644 index 0000000000..98cce30520 --- /dev/null +++ b/research/physical-inverse-pair/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-inverse-fixed-grid/PROOF.md", + "research/coded-native-caller/CODE.json", + "research/coded-native-caller/NORMALIZERS.json", + "research/coded-native-caller/PHYSICAL.md", + "research/coded-reverse-controller/verify.py", + "research/coded-reverse-physical-pair-gap/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source signs, eight width1/2 Walsh fibers, all 224 main input columns, mixed inputs, boundary-order and helper-erasure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Identical checks under optimized Python." + } + ] +} diff --git a/research/physical-inverse-pair/verify.py b/research/physical-inverse-pair/verify.py new file mode 100644 index 0000000000..6493b0e2c9 --- /dev/null +++ b/research/physical-inverse-pair/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Source-bound one-pair check; standard library, no Git or native replay. + +Apache-2.0. JoyboyBrian with substantial OpenAI Codex assistance. +""" +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path +import argparse +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P = 65537 +J = 256 +N = 112 + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def parity(x): + return x.bit_count() & 1 + + +def mv(rows, x): + return sum(parity(r & x) << j for j, r in enumerate(rows)) + + +def transpose(rows): + return [sum(((r >> j) & 1) << k for k, r in enumerate(rows)) for j in range(9)] + + +def mix(x, columns, inverse=False): + # All source reads finish before the first owner update. + modes = [sum(s * x[i] for i, s in c) % P for c in columns] + out = list(x) + scale = pow(52 if inverse else 4, -1, P) + for c, t in zip(columns, modes): + for i, s in c: + out[i] = (out[i] - s * scale * t) % P + return out + + +def diagonal(d, x): + return [a * b % P for a, b in zip(d, x)] + + +def plus(x, y, sign=1): + return [(a + sign * b) % P for a, b in zip(x, y)] + + +def pair(x, y, q, d, columns, omit_exit_q=False, omit_entry=False, wrong_order=False): + qi = [pow(v, -1, P) for v in q] + y = list(y) if omit_entry else mix(y, columns, True) + x = diagonal(d, plus(x, diagonal(q, mix(y, columns)), -1)) + y = diagonal(d, y) + source = diagonal(qi, mix(x, columns, True)) + if wrong_order: + source = mix(diagonal(qi, x), columns, True) + y = plus(y, source) + y = mix(y, columns) if omit_exit_q else diagonal(qi, mix(diagonal(q, y), columns)) + return x, y + + +def standard(x, y, q, d): + return (diagonal(d, plus(x, diagonal(q, y), -1)), + diagonal(d, diagonal([pow(v, -1, P) for v in q], x))) + + +def cleanup(targets): + owned = {('query', i) for i in range(N)} | {('mode', i) for i in range(8)} + need(all(t in owned for t in targets), 'Cleanup must not address arbitrary helper/main input') + + +def run(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for source in manifest['files']: + if source['usage'] == 'input': + need(sha256((ROOT / source['path']).read_bytes()).hexdigest() == source['sha256'], + 'Pinned source mismatch: ' + source['path']) + receipt = json.loads((ROOT / 'research/coded-native-caller/NORMALIZERS.json').read_text()) + records = receipt['ports'] + modes = receipt['mode_columns'] + a = [[Fraction(v) for v in r] for r in json.loads( + (ROOT / 'research/coded-native-caller/CODE.json').read_text())['A']] + need(len(records) == N and len(modes) == 8, 'Source dimensions') + need(all(len(c) == N and sum(bool(v) for v in c) == 56 for c in modes), 'Mode incidence') + need(all(sum(bool(c[i]) for c in modes) == 4 for i in range(N)), 'Owner incidence') + need(all(sum(x*y for x, y in zip(c, e)) == 56*(i == j) + for i, c in enumerate(modes) for j, e in enumerate(modes)), 'Mode Gram identity') + need(all(a[i][j] == (i == j)-Fraction(sum(c[i]*c[j] for c in modes), 4) + for i in range(N) for j in range(N)), 'Every exact code entry') + need(J*J % P == P-1, 'Gaussian rational finite-field embedding') + columns = [[(i, s) for i, s in enumerate(c) if s] for c in modes] + normalizer_checks = 0 + for i, rec in enumerate(records): + rows, z = rec['G_rows'], rec['Z_mask'] + gt = transpose(rows) + need(rec['port'] == i and mv(rows, 1) == rec['q'], 'Actual source owner port') + need(all(parity(r & s) == (j == k) for j, r in enumerate(rows) + for k, s in enumerate(rows)), 'Orthogonal source K') + for u in range(512): + # Direct Walsh action of Z_z P_G, independently from an assumed commutator. + v = mv(gt, u ^ z) + need((v.bit_count()-u.bit_count()) % 4 == 0, 'Signed K preserves absolute R phase') + normalizer_checks += 1 + ri, rj = records[:2] + u = mv(rj['G_rows'], 1) + s = 1-2*parity(rj['Z_mask'] & u) + v = mv(transpose(ri['G_rows']), u) + s *= 1-2*parity(ri['Z_mask'] & u) + need((v, s*a[0][1]) == (22, Fraction(1, 2)), 'Literal signed C01 address1 witness') + need(v != 1 and a[0][1] == -Fraction(1, 2), 'Old scalar A^-1 recipe remains rejected') + unsigned_rejected = any(mv(transpose(r['G_rows']), u).bit_count() % 4 != u.bit_count() % 4 + for r in records for u in range(512)) + need(unsigned_rejected, 'Omitting K signs must fail absolute-phase centralization') + fibers = [(0,), (1,), (19,), (511,), (0, 1), (1, 19), (17, 256), (511, 511)] + rejected = {'omit_exit_q': False, 'omit_entry': False, 'wrong_order': False} + basis_checks = 0 + for frequency in fibers: + physical = [tuple(mv(transpose(r['G_rows']), u ^ r['Z_mask']) for u in frequency) + for r in records] + q = [pow(J, sum(v & 1 for v in row), P) for row in physical] + d = [pow(J, sum((v >> 1).bit_count() for v in row), P) for row in physical] + need(all(qi*di % P == pow(J, sum(u.bit_count() for u in frequency), P) + for qi, di in zip(q, d)), 'Actual DQ constant on source fiber') + for col in range(2*N): + x, y = [0]*N, [0]*N + (x if col < N else y)[col % N] = 1 + want = standard(x, y, q, d) + need(pair(x, y, q, d, columns) == want, 'All four blocks on independent basis column') + basis_checks += 1 + for mutant in rejected: + if not rejected[mutant]: + rejected[mutant] = pair(x, y, q, d, columns, **{mutant: True}) != want + x, y = [(i*i+3) % P for i in range(N)], [(7*i+11) % P for i in range(N)] + need(pair(x, y, q, d, columns) == standard(x, y, q, d), 'Mixed arbitrary owner inputs') + need(all(rejected.values()), 'Every semantic mutant must be distinguished') + # The physical delta at owner1/address1 has all 512 Walsh frequencies. + for frequency in range(512): + physical = [mv(transpose(r['G_rows']), frequency ^ r['Z_mask']) for r in records] + q = [pow(J, v & 1, P) for v in physical] + d = [pow(J, (v >> 1).bit_count(), P) for v in physical] + x, y = [0]*N, [0]*N + y[1] = (1-2*(physical[1] & 1))*pow(512, -1, P) % P + need(pair(x, y, q, d, columns) == standard(x, y, q, d), + 'Every Walsh coefficient of physical owner1/address1 input') + clean = [('mode', i) for _ in range(6) for i in range(8)] + clean += [('query', i) for _ in range(2) for i in range(N)] + cleanup(clean) + try: + cleanup(clean + [('helper', 17)]) + except ValueError: + pass + else: + raise ValueError('Illegal helper erasure accepted') + return { + 'status': 'PASS_PHYSICAL_INVERSE_PAIR', 'scope': 'One-stage exact operator identity; conditional physical ledger, no new kappa', + 'normalizer_absolute_phase_checks': normalizer_checks, + 'widths': [1, 2], 'walsh_fibers': [list(v) for v in fibers], + 'independent_main_basis_columns': basis_checks, + 'physical_address1_walsh_coefficients': 512, 'mixed_input_checks': len(fibers), 'helpers': '408 inherited autonomous output operators; never scratch', + 'semantic_rejections': list(rejected) + ['unsigned_K', 'old_scalar_A', 'helper_erasure'], + 'added_paid_rank1_jobs': 336, 'total_paid_profile': {'1':2537, '2':412, '3':510, '4':127, '5':40}, + 'wrapper_monomial_maps_upper': 1792, 'scalar_adds': 2800, + 'recoding_owned_clears': 48, 'query_initial_clears':112, 'query_copies':112, 'query_owned_erases':112, + 'recoding_field_workspace':120, 'inverse_recode_calls':2, 'forward_recode_calls':1, + 'unknown_nonzero_costs': ['Native/query internal scratch and movement', 'Physical field-map and rational ADD tape tariffs', 'Finite precision and global error budget', 'Full-controller bridge and boundary accounting']} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = run() + path = HERE / 'RESULT.json' + if args.write: + path.write_text(json.dumps(result, indent=2)+'\n') + else: + need(json.loads(path.read_text()) == result, 'Committed mathematical receipt differs') + print(json.dumps(result, sort_keys=True))