diff --git a/research/joint-query/NOTICE.md b/research/joint-query/NOTICE.md new file mode 100644 index 0000000000..297ac2775c --- /dev/null +++ b/research/joint-query/NOTICE.md @@ -0,0 +1,45 @@ +# Source attribution and license + +New research, code, and verification used substantial OpenAI Codex +assistance under the user's direction. Separate agents developed and +reviewed the algebra, scalar words, owner maps, and native phases. +The recorded independent reviews are agent reviews. No independent +human review is claimed. New material uses the repository's Apache-2.0 +license, retained in [notices/LICENSE](notices/LICENSE). + +The local word and phase data come from the gauge44 and t16 source +lineage at commit bce54fb3f895cbe5cd4c0eb477c3afeed100190f. Their original +notices are copied without changes: + +- [Gauge44 notice](notices/research/gauge44-slots-t16/NOTICE.md). +- [Construction notice](notices/research/gauge44-slots-t16/construction/NOTICE.md). +- [T16 integration notice](notices/research/gauge44-slots-t16/t16/NOTICE.md). +- [Complete upstream notice](notices/research/gauge44-slots-t16/UPSTREAM-NOTICE.md). + +Those notices preserve the credited contributors, predecessor results, +licenses, source pins, and earlier AI disclosures. This package does not +claim those results as new work. + +The source loader is unchanged from research/native-source-codes at +commit 7649d9ceecec949541bec4bbde5929344166ba59. The new package does not +change that package or depend on its four example programs. It reads the +same immutable source archive directly. + +The centre-encoding campaign first supplied the selected-section and +source-code constructions. The cover-algebra lane supplied the ordered +joint-query theorem and inverses. The residual-syndrome lane supplied the +short scalar words and independent scalar review. The coherent-port lane +supplied the native component lowering and proof review. The +circuit-interface lane supplied the frozen full-cover words. The +residual-syndrome independent reviewer supplied the full native review. +The interface-proof lane supplied the inherited bridge proof and the +independent controller witness review. The encoded-controller lane +supplied the selected-observation witness. These source files and their +exact hashes are recorded in [SOURCES.json](SOURCES.json). + +The portable scalar, native, and ordered checkers adapt those proof and +independent review methods. They do not import the exploratory emitters. +The sixteen-port construction follows the earlier source-only logger; +its use of joint X and Y state is a separate local construction. No +controller closure, complete supplier gain, or official frontier change +is claimed. diff --git a/research/joint-query/README.md b/research/joint-query/README.md new file mode 100644 index 0000000000..2bf4fc0aa2 --- /dev/null +++ b/research/joint-query/README.md @@ -0,0 +1,153 @@ +# Local joint-query transfer through sixteen existing ports + +This package gives invertible local forward and backward words that use +sixteen existing data ports to carry centre queries. They change the +selected source baseline and use joint X and Y state. The ordered proof +does not require an inverse of the ordinary response matrix M. This +removes the Schur-unit requirement of the earlier fixed-baseline model +for this local construction family. + +The [ordered proof](evidence/JOINT-QUERY-TRANSFER.md) gives the precise +hypotheses, maps, and inverses. The [native contract](evidence/CONSERVED-QQ16.md) +gives the full-cover action and sweep order. The frozen words passed +[independent scalar review](evidence/SCALAR-REVIEW.md) and +[independent native review](evidence/NATIVE-REVIEW.md). The native review +supersedes the older pending-review sentence in the frozen native note. +The [independent package audit](evidence/PACKAGE-REVIEW.md) also passed. +It checks the portable adaptation and a copied-directory cold replay. + +The construction does not close the changing-chart controller. It does +not establish a complete supplier or a new kappa bound. + +## Query contract + +The two disjoint selected sets are + +```text +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110]. +``` + +Use the actual 8 by 112 centre matrix R, K=R^T/4, and J=I-KR. +The A and T minors have dyadic inverses. The ordinary set U has 96 ports, +and R K_U=12I. Each current chart s has the routed operators R_s, K_s, +and selected query ell_s. A future chart t has the A logger E_t. + +The backward word has u=E_t y, a=ell_s x, and b=R_s u. It returns + +```text +R_s y' = a, +ell_(t,A) y' = R_t y, +ell_s x' = b + 12a. +``` + +These are different records. The selected X result is not b alone. +The forward word returns the full current X query in T and moves the +old T query into A. Both words preserve X_p+Y_p for all p in A union T. +Their displayed data inverses work in both orders. The forward and +backward words are companions; they are not inverse circuits. + +The general ordered theorem replaces 12I by M=R K_U. It uses only the +stated selected sections and support conditions. M may be singular. +The portable tests include the actual R, a noncentral matrix M, and M=0. +The ring proof, not these finite examples, establishes the general claim. + +## Native and workspace contract + +The certificate contains all 28 B_s_t words for 1 <= s < t <= 8 and all +nine F_s words for 0 <= s <= 8. A cover map changes the owner and applies +its separate payload translation on every tensor layer. It is not a +payload permutation of one fixed owner array. + +Each cover sweep must finish before the next event. Each private sweep +executes its whole row body at one owner before it moves to the next +owner. The new wrappers use one existing owned C0 field, with a clear +before and after each row. They allocate no new field. All 480 arbitrary +ordinary helpers are restored. The eight owned private inputs may be +arbitrary; the complete word discards them and returns zero. They are +not claimed to be borrowed inputs that must be restored. + +| Complete local word | Real scalar primitive bound | Added rank-one children | Native rank mass | Added full-cover maps | Native wrapper maps | +|---|---:|---:|---:|---:|---:| +| B_s_t | 214986 | 24 | 5546 | 528 | 48 | +| F_s, s > 0 | 211210 | 8 | 5530 | 288 | 16 | +| F_0 | 211210 | 8 | 5530 | 0 | 16 | + +These counts include the retained core. Each core costs 202138 scalar +primitives and has native mass 5522. The map columns count operations; +they are not a physical stream or address implementation cost. The +formal scalar prefix guards are 73 bits for B and 55 bits for F. They +are not a recursive precision proof. + +## Reproduce + +Use Python 3.10 or later, its standard library, and Git. The repository +must contain commit bce54fb3f895cbe5cd4c0eb477c3afeed100190f and its +selected-replay archive. No network, package installation, scratch lane, +or predecessor Python package is used at runtime. Run one process. + +From a checkout that contains this package at research/joint-query: + +```sh +python3 -I -O -B research/joint-query/replay.py --repo . --out /tmp/qq16-replay +``` + +Expected first line: + +```text +PASS_PORTABLE_QQ16_LOCAL_JOINT_QUERY +``` + +The entrypoint rebuilds R and both clean-J cores from the immutable Git +archive. It then rebuilds every added scalar coefficient and all 1008 +chart routes from the actual source phase data. It checks: + +- both 712-column scalar maps, all helper outputs, both data inverse + orders, two algebraic compositions, and sixteen conserved sums; +- all 37 literal owner paths, private lifetimes, exact frame polynomials, + and the complete local scalar and native invoices; +- all 16384 Gaussian basis columns of the 32 signed native line recipes; +- timing, private-clear, scalar-phase, inverse-sign, translation, + owner-action, and odd-denominator controls. + +All validation remains active under -O. The output JSON files record +the source and code hashes. [SOURCES.json](SOURCES.json) records the +original proof and review dependencies and their exact hash modes. + +## Scope and open obligations + +The retained core bytes, scalar maps, and local frame ledger are checked +again. The [bridge proof](evidence/BRIDGE-REVIEW.md) supplies the inherited +owner embedding and endpoint adapters. The old recursive child kernels +are not rerun by this package. The algebraic inverse formulas do not give +free legal reads from the native output frames. + +The [selected-observation witness](evidence/QQ16-SELECTED-WITNESS.md) +blocks the current conserved controller with its fixed first F0/B1 pair +and retained ordinary bank schedule. It still blocks later homogeneous +selected-only linear controls when all five F query histories are given. +It does not exclude a changed first pair, ordinary-to-selected reads, +affine helper state, or paid query operations. Its +[independent review](evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md) is +retained evidence; this entrypoint does not rerun that global witness. + +New child and helper hosting, controller closure, endpoint recovery, +stream and address costs, recursive precision, and the complete supplier +invoice remain open. The separately reviewed map-fusion follow-up is not +included in this base certificate. Source credits and AI assistance are +recorded in [NOTICE.md](NOTICE.md). + +## Open next questions + +Can a changed local interface retain the old chart queries through the +whole controller? The first step is an ordered inverse calculation with +explicit selected records. The fixed first-pair witness blocks the +current conserved interface and its stated observation set. + +Can new children use the actual owner and helper schedule? Bind each +child to an owner, prove each private lifetime, and check each complete +cover sweep. The local certificate does not supply that global layout. + +Does a complete construction reduce the supplier cost? After controller +closure, count all storage, address maps, scalar work, precision and +recursive children. The local count alone does not settle this question. diff --git a/research/joint-query/SOURCES.json b/research/joint-query/SOURCES.json new file mode 100644 index 0000000000..3e66629292 --- /dev/null +++ b/research/joint-query/SOURCES.json @@ -0,0 +1,165 @@ +{ + "AI_assistance": "Research, implementation, and verification used substantial OpenAI Codex assistance. Separate agents supplied the recorded reviews; no independent human review is claimed.", + "adapted_checkers": { + "verify_native.py": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/native/verify_native_review.py", + "source_sha256": "a4029bc65ac4149adc7043dc6da254e03630dc0037d32c903058162c46003c16" + }, + "verify_ordered.py": { + "campaign_source": "lanes/cover-algebra/check_joint_query_transfer.py", + "source_sha256": "fb60403444aa0a7cea8c1a3774a4aa85fb238013dd94796f8ffd4020c68f4073" + }, + "verify_scalar.py": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/verify_conserved_review.py", + "source_sha256": "4bbbefd65cc06a3120bc30072979e6597dd002460a952385bde7e98196ea9fb9" + } + }, + "chart_reconstruction": "The 112 local chart bases and all 1008 routes are rebuilt from the pinned single-layer DATA-PHASES source. The frozen packet consumed doubled chart payload 498d85807dd3032de01b5da72a67717f02ee0ecf068e8c47f67d4f21034cd896. Both supply the same local bases.", + "evidence": { + "evidence/BRIDGE-OPERATOR-REVIEW.json": { + "campaign_source": "lanes/interface-proof/BRIDGE-OPERATOR-REVIEW.json", + "role": "Inherited exact bridge and source binding receipt", + "sha256": "c905a19d70f34c435c5f5454c6190bbfb1ce4594b1513bf76156acf620d7c6fc" + }, + "evidence/BRIDGE-REVIEW.md": { + "campaign_source": "lanes/interface-proof/BRIDGE-REVIEW.md", + "role": "Inherited owner and core embedding proof", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + }, + "evidence/CONSERVED-QQ16.json": { + "campaign_source": "lanes/circuit-interface/qq16/CONSERVED-QQ16.json", + "role": "Original full native producer receipt", + "sha256": "b91eb8599c403db55c889bb225a1cd93f46fdb83eb339f101d18843d52b1c920" + }, + "evidence/CONSERVED-QQ16.md": { + "campaign_source": "lanes/circuit-interface/qq16/CONSERVED-QQ16.md", + "role": "Frozen native contract; later independent review supersedes its pending status", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + "evidence/JOINT-QUERY-TRANSFER-REVIEW.json": { + "campaign_source": "lanes/coherent-port/JOINT-QUERY-TRANSFER-REVIEW.json", + "role": "Independent ordered proof review", + "sha256": "28d9d525c9eec07c91cb51edfdb5a0cf01ff75fddd39046b3d2fda03456e9153" + }, + "evidence/JOINT-QUERY-TRANSFER.json": { + "campaign_source": "lanes/cover-algebra/JOINT-QUERY-TRANSFER.json", + "role": "Original ordered regression receipt", + "sha256": "1f32819591103ab323c69cf50cf6579b0e881e105ca4a93b48125d5b89214c31" + }, + "evidence/JOINT-QUERY-TRANSFER.md": { + "campaign_source": "lanes/cover-algebra/JOINT-QUERY-TRANSFER.md", + "role": "Ordered ring proof and exact maps", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + "evidence/NATIVE-REVIEW.json": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/native/REVIEW.json", + "role": "Independent full native receipt", + "sha256": "e9e9287a4a4d1be3c802899a42f70ff5dd5efd1e144a48bd585386fe234832e5" + }, + "evidence/NATIVE-REVIEW.md": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/native/REVIEW.md", + "role": "Independent full native review", + "sha256": "2247e3cbe73f3f0da55c647ffae15f98dd9445b2366ba9e255b9bebc9f742b70" + }, + "evidence/QQ16-COVER-ACTION-ADDENDUM.md": { + "campaign_source": "lanes/coherent-port/QQ16-COVER-ACTION-ADDENDUM.md", + "role": "Exact distinction between owner routes and payload permutations", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + "evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.json": { + "campaign_source": "lanes/interface-proof/rational-decoder/QQ16-RATIONAL-OBSERVATION-REVIEW.json", + "role": "Independent controller witness receipt", + "sha256": "588a3ce4593576ae921e97c6ced6a050f88736f29708cfee117385b254cd358f" + }, + "evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md": { + "campaign_source": "lanes/interface-proof/rational-decoder/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "role": "Independent controller witness proof review", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + "evidence/QQ16-SELECTED-WITNESS.json": { + "campaign_source": "lanes/encoded-controller/QQ16-SELECTED-WITNESS.json", + "role": "Controller witness receipt", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + "evidence/QQ16-SELECTED-WITNESS.md": { + "campaign_source": "lanes/encoded-controller/QQ16-SELECTED-WITNESS.md", + "role": "Current controller obstruction and exact scope", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + }, + "evidence/SCALAR-REVIEW.json": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/REVIEW.json", + "role": "Independent scalar receipt", + "sha256": "171bdbec200359c82aba79e4153d73bfcbf14ac3ae4e07b15476b79b7fcbf091" + }, + "evidence/SCALAR-REVIEW.md": { + "campaign_source": "lanes/residual-syndrome/physical-algebra/review-gauss/conserved-qq16/REVIEW.md", + "role": "Independent scalar proof review", + "sha256": "aa7b9f74430b56c42e1099029a501a9b6be9ab56b81bfdc681e4c2e6ff5bc97d" + }, + "notices/LICENSE": { + "git_source": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f:LICENSE", + "role": "Unchanged source notice or license", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + "notices/research/gauge44-slots-t16/NOTICE.md": { + "git_source": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f:research/gauge44-slots-t16/NOTICE.md", + "role": "Unchanged source notice or license", + "sha256": "7a8d17b04da1e6c9d0ec217fb5bda72faa09d9a21695128722dd1e2827870fcf" + }, + "notices/research/gauge44-slots-t16/UPSTREAM-NOTICE.md": { + "git_source": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f:research/gauge44-slots-t16/UPSTREAM-NOTICE.md", + "role": "Unchanged source notice or license", + "sha256": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610" + }, + "notices/research/gauge44-slots-t16/construction/NOTICE.md": { + "git_source": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f:research/gauge44-slots-t16/construction/NOTICE.md", + "role": "Unchanged source notice or license", + "sha256": "defe7e44af610e25a6c50c1c3b2efd0972d0690574995c0c872fc50eebf4c816" + }, + "notices/research/gauge44-slots-t16/t16/NOTICE.md": { + "git_source": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f:research/gauge44-slots-t16/t16/NOTICE.md", + "role": "Unchanged source notice or license", + "sha256": "902370e6bfcd39dbea2ece474f15fccbcce3b8e966b2b94066bd03e5174591b5" + } + }, + "native_certificate": { + "campaign_source": "lanes/circuit-interface/qq16/CONSERVED-QQ16-PROGRAMS.json.gz", + "decompressed_sha256": "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef", + "file_sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + "original_source_audit": { + "campaign_source": "lanes/circuit-interface/qq16/SOURCE-BUNDLE.json", + "scope": "All 31 direct source files and their hash modes were checked before packaging. Absolute workspace paths are omitted from this portable package.", + "sha256": "6654c7a2cf68c20963c2eb36da4dda039a6afa16a6f894e170dd58dfa5cc63cf" + }, + "portable_loader": { + "sha256": "d23924511e3aed41e5e64511ca70126a636d91c8aa02e656cb61d6ceca1fe0a0", + "source_commit": "7649d9ceecec949541bec4bbde5929344166ba59", + "source_path": "research/native-source-codes/source_data.py" + }, + "review_boundary": "Original independent receipts are preserved. The new portable adaptation needs its own independent review.", + "schema": "portable-qq16-source-manifest-v1", + "source": { + "archive_path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "credit_sources": { + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "research/gauge44-slots-t16/NOTICE.md": "7a8d17b04da1e6c9d0ec217fb5bda72faa09d9a21695128722dd1e2827870fcf", + "research/gauge44-slots-t16/UPSTREAM-NOTICE.md": "a75967ebc34e3bf2ff2c25c08e6c7f1a61b0c0d171cfd1b62196ae2caaf2c610", + "research/gauge44-slots-t16/construction/NOTICE.md": "defe7e44af610e25a6c50c1c3b2efd0972d0690574995c0c872fc50eebf4c816", + "research/gauge44-slots-t16/t16/NOTICE.md": "902370e6bfcd39dbea2ece474f15fccbcce3b8e966b2b94066bd03e5174591b5" + }, + "decompressed_payloads": { + "CANONICAL-WORD.json.gz": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c", + "LOCAL-PROGRAMS.json.gz": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3" + }, + "members": { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/CLIFFORD-RECIPES.json": "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731", + "slots/local/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "slots/local/RESIDUAL-ADAPTERS.json": "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + } + } +} diff --git a/research/joint-query/certificate.json.gz b/research/joint-query/certificate.json.gz new file mode 100644 index 0000000000..c6e876d8b4 Binary files /dev/null and b/research/joint-query/certificate.json.gz differ diff --git a/research/joint-query/evidence/BRIDGE-OPERATOR-REVIEW.json b/research/joint-query/evidence/BRIDGE-OPERATOR-REVIEW.json new file mode 100644 index 0000000000..bdd8781819 --- /dev/null +++ b/research/joint-query/evidence/BRIDGE-OPERATOR-REVIEW.json @@ -0,0 +1,73 @@ +{ + "actual_data_owner_routes_checked": 32256, + "actual_local_shear": "D L(J) D or D U(-J^T) D in the pinned boundary gauges", + "actual_stage_entry_exit_gauges_checked": 1008, + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "complete_phase_identity_character_checks": 51744, + "divide13_finite_bit_circuit": { + "divisor": 13, + "exactness_condition": "Input numerator is divisible by 13 under the common odd-grid invariant", + "excluded_costs": [ + "stream reads and writes", + "address routing", + "root common-grid conversions" + ], + "extra_finite_control_bits_upper_bound": 32, + "nondivisible_inputs_with_nonzero_remainder": 15123, + "scan_order": "Conditional negation from low to high; unsigned division from high to low; conditional negation from low to high", + "signed_14_bit_inputs_checked": 16384, + "signed_AND_OR_NOT_gates_per_numerator_bit": 179, + "unsigned_AND_OR_NOT_gates_per_numerator_bit": 161, + "valid_state_transitions": 26 + }, + "interface_sha256": "5c6c51fbffc07a683e922f17532fd90262ae9e23cc3560a696002073dd234ef3", + "logical_bridge": "A^-1 J A T_boundary=T_boundary D J D; the same identity holds for J^-1", + "maximum_resident_bytes": 182386688, + "operator_alignment": "A=Z_delta D; A T_boundary=T_common D", + "phase_controls": { + "omitted_X_translation_rejected": 112, + "omitted_Y_translation_rejected": 112, + "reversed_Y_route_translation_order_rejected": 112 + }, + "phase_method": "Exact Fourier-character evaluation on all weight-zero, one, and two inputs in the active 17-dimensional space", + "scalar_programs": { + "forward": { + "additional_real_divide_by_13_streams": 0, + "dyadic_real_primitive_bound": 7232, + "events": 920, + "full_input_columns_checked": 113, + "macros": { + "add": 896, + "clear": 16, + "quarter": 8 + }, + "maximum_live_private_arrays": 1, + "native_children": 0, + "private_input_and_output_zero": true + }, + "inverse": { + "additional_real_divide_by_13_streams": 16, + "dyadic_real_primitive_bound": 7232, + "events": 928, + "full_input_columns_checked": 113, + "macros": { + "add": 896, + "clear": 16, + "divide13": 8, + "quarter": 8 + }, + "maximum_live_private_arrays": 1, + "native_children": 0, + "private_input_and_output_zero": true + } + }, + "scope": "Exact native operator and finite scalar macro invoice. Address routing, bit division cost, and a complete controller invoice remain separate.", + "seconds": 4.192791291999583, + "source_base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "source_pins": { + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "t16/global/hosted/GLOBAL-TEMPLATE.json.gz": "73f47a1e60b1e4ea66dbca9a497c411c8e6adc7984e276a437a10a9a7a13b47a" + }, + "status": "PASS_EXACT_BRIDGE_OPERATORS_AND_ACTUAL_LOCAL_GAUGE", + "two_factor_phase_checks": 17248 +} diff --git a/research/joint-query/evidence/BRIDGE-REVIEW.md b/research/joint-query/evidence/BRIDGE-REVIEW.md new file mode 100644 index 0000000000..86139908c4 --- /dev/null +++ b/research/joint-query/evidence/BRIDGE-REVIEW.md @@ -0,0 +1,235 @@ +# Exact operators for the phase-aware bridges + +The bridge construction in `../cover-algebra/BRIDGES.md` implements the same +logical operator K_t as the centre-free local word. It does not leave a Pauli +conjugation in the logical content. This conclusion requires both listed +translation corrections in the stated order. A bare cover permutation does +not give the result. + +`BRIDGE-OPERATOR-REVIEW.json` records an independent check. The checker imports +none of the route, bridge, or Clifford checkers. It reads the actual phase +recipes and hosted template from the +[pinned replay archive](https://github.com/CrocSwap/integer-mult-bounds/blob/bce54fb3f895cbe5cd4c0eb477c3afeed100190f/research/community-frontier1042-audit/selected-replay.tar.gz). +The archive hash is `22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754`. +The receipt also records the hashes of both source members and the centre +matrix. This note is an operator review and a finite scalar invoice. It does +not admit a complete recursive supplier. + +## 1. Native conventions + +Let T_a be address translation by a. The native line operator is + + C_a = (1+i) I/2 + (1-i) T_a/2. + +On the Fourier character indexed by u, its multiplier is i^(a dot u), where +the binary dot product is read as the integer zero or one. Hence a signed +product of line operators has multiplier i^phi(u), with + + phi(u) = sum_j epsilon_j (a_j dot u) modulo 4. + +All operators here fix the constant character. There is no undetermined +global phase. A translation T_delta has multiplier (-1)^(delta dot u). + +For an orthonormal coordinate space U, let F_U be the product of its +coordinate line operators. At a completed stage s, the boundary gauges are + + X at port q and cover d: F_(d U_s), + Y at port q and cover d: F_(d U_s) C_(d q)^-1. + +Here U_s=L+E_1+...+E_s, dim(L)=9, and dim(E_t)=8. The initial gauges are +C_(d q) on X and I on Y. These are the selected controller conventions. +The source check below binds the local entry and exit adapters to them. +It does not independently repeat the entire idle-child schedule proof. + +Write B_q for the eight orthonormal chart columns in q-perp. The actual +involution rho_t(q) fixes q, swaps these columns with E_t, and fixes the +other external blocks. Let + + beta_q[i] = (weight(B_q[i])-1)/2 modulo 2. + +The review checks the following complete operator identities: + + rho_t(F_(U_s) C_q^-1) = T_(q+lift_t(beta_q)) F_(E_1+...+E_s+E_t), s=t. + +The notation rho_t(F) means transport of every axis of F by rho_t. The +other external blocks are fixed, so their identical factors cancel from +each equation. It is enough to check the 17 coordinates in L+E_t. + +The checker evaluates the full phase at zero, at every unit vector, and at +every sum of two distinct unit vectors. This determines the complete phase: +the integer expansion of a binary parity modulo four has degree at most two. +It gives 51,744 exact character checks for the two bridge identities and the +source entrance identity. Omission of either correction is rejected for all +112 ports. Reversal of the Y route and correction order is also rejected +for every port. There are 17,248 additional two-factor phase checks. + +## 2. Which logical operator the bridge performs + +Let T be one of the boundary gauges above, as a block diagonal operator on +all port-cover positions. Define D by + + (D v)_(d,q) = v_(d rho_t(q),q). + +This operation only changes the selected cover position. It does not apply +rho_t to the payload address. These are independent input arrays, and their +contents must remain distinct. + +Let Z be the block translation whose component at (d,q) is T_(d delta_q), +with delta from section 1. Put A=ZD. The exact phase identities give + + A T = T_common D. + +At each fixed cover d, T_common is independent of q. Therefore every scalar +port matrix M commutes with it. In particular, + + (A^-1 M A) T = T D M D. + +Since D is an involution and translations are involutions, the physical +sequence is D, then Z, then M, then Z, then D. On logical content its result +is exactly D M D. For M=J or M=J^-1 this is K_t or K_t^-1. The result holds +on Y before stage t and on X at or after stage t. It is valid at all cover +positions and on arbitrary payloads. + +This proof also gives the general construction: any port matrix that has a +finite scalar implementation can be applied after alignment. Only its +coefficient and workspace costs change. Inverses and products use the same +logical gauges; each individual bridge returns to the original gauge. + +## 3. Binding to the actual local shear + +For t>0, the exact `DATA-PHASES.json` entries in owner coordinates are + + entry_X = entry_Y = q + B_q beta_q, + exit_X = exit_Y = B_q beta_q + lift_t(beta_q). + +The stage-zero entries are all zero. The independent check verifies all +1,008 port-stage recipes against these formulas. It also checks all 32,256 +data owner routes in the hosted template. The source template refers to +this exact phase file and uses physical cover position d rho_t(q). + +An owner-coordinate translation a is a translation by d rho_t(q) a in the +local cover sweep at d. Thus the entry correction is physically +T_(d(q+lift_t(beta_q))). The exit vector is rho_t-invariant, so its physical +correction is T_(d(B_q beta_q+lift_t(beta_q))). + +After routing and the entry correction, X has native frame C_(d q) times +the common exterior factor, and Y has just that common exterior factor. +The local word thus receives its exact native entry gauges. Its scalar +forward map is L(J), and its backward map is U(-J^T). The exact local review +in `PROOF.md` proves these maps on arbitrary data and helper values. At exit, +both words have their prescribed full local frames. The exit correction +converts these frames to the routed global boundary frames. Routing back +therefore gives + + D L(J) D, or D U(-J^T) D. + +Their off-diagonal coefficient is exactly K_t=D J D, or its transpose with +the backward sign. This is the same K_t as section 2. No payload permutation +or leftover translation has been removed by assumption. + +## 4. Tensor powers and legal access + +Replace every native frame and translation by its lambda-th tensor power. +Every operator equality above remains an equality. The scalar port matrix +acts on the port coordinate and commutes with the tensor address operators. +Its coefficients stay unchanged; they are not raised to power lambda. +Identity spectator factors can be added throughout. This proves the result +for every positive integer lambda and arbitrary spectator contents. + +The cover route and translation can also define a view of the data array. +For each fixed port they are bijections. Distinct routed cover blocks thus +do not overlap, and gathering one block before its update is legal. A direct +implementation can use these views for its source reads and target writes; +it need not materialize a full additional data bank. This statement does not +make address computation free. The supplier must price the route, the +repeated tensor translation, stream access, and any physical realization. + +One private accumulator suffices for the scalar step below. Its physical +contents are cleared before use, so it can carry the common frame without +a native preparation child. The final clear restores it to zero. No +assumption is made about its initial contents. No other borrowed register +is changed by the scalar step. + +## 5. A one-accumulator scalar implementation + +Let r_k be row k of R. The exact relation R R^T=56I gives r_j r_k^T=0 for +j different from k. Consequently the following eight row updates commute: + + v <- v - r_k^T (r_k v)/4. + +An earlier row update does not change a later row sum. Their product is +J=I-R^T R/4. Replacing 4 by 52 gives J^-1, since + + (I-R^T R/4)(I-R^T R/52)=I. + +For each row, clear one private accumulator, gather r_k v, divide the +accumulator by 4, scatter its signed value by -r_k^T, and clear it. For the +inverse, also divide the accumulator by 13 before the scatter. The source +matrix has 448 nonzero entries, all plus or minus one. + +| Item per port-cover block | J | J^-1 | +|---|---:|---:| +| Signed ADD macros | 896 | 896 | +| Divide-by-four SCALE macros | 8 | 8 | +| CLEAR macros | 16 | 16 | +| Complex divide-by-13 scans | 0 | 8 | +| Maximum live private arrays | 1 | 1 | +| Added native children | 0 | 0 | + +Under the retained primitive bounds, each signed ADD costs at most four +real primitives, each divide-by-four SCALE costs two, and each CLEAR costs +one. Including both real components gives 7,232 real primitives. The inverse +adds 16 real constant-division scans. Both emitted abstract scalar programs +were replayed on all 113 input columns. This includes the arbitrary private +input. The output private row and its input column are zero. Omitting the +first clear or the first inverse division fails the full map check. + +The current dyadic compiler does not admit division by 13. Section 3 of +`COEFFICIENTS.md` identifies the repository's common odd-grid construction. +It applies with a fixed factor 13. This is an extension that must be included +in the changed compiler and recursive precision proof. + +There is a concrete finite bit circuit for that division. In unsigned binary +long division, the state is a remainder r in {0,...,12}. On input bit b, +emit floor((2r+b)/13) and keep (2r+b) modulo 13. A truth-table circuit for +these 26 cases uses 161 two-input AND/OR or one-input NOT gates per bit. +Two conditional-negation scans handle a signed two's-complement numerator. +Each uses at most nine such gates per bit. Thus a signed ell-bit division +uses at most 179 ell Boolean gates, three linear scans, and at most 32 bits +of extra finite control. Stream reads, writes, and addressing are separate. +The checker verifies all 26 transitions and all 16,384 signed 14-bit inputs. +Nondivisible inputs have a nonzero remainder; they are not silently accepted. + +Exactness on the supplier follows from the common-grid invariant, not from +arbitrary integer divisibility. Choose enough root factors of 13 for the +maximum unfinished recursion chain. Completed native children are Gaussian +dyadic and do not consume this reserve. Every division input numerator is +then divisible by 13. Root scaling and final unscaling remain part of the +complete assembly bill. The bridge alone does not prove this recursive +invariant for a proposed whole controller. + +## 6. Review result and remaining work + +No material phase or logical-operator defect was found in this bridge +construction. Its exact scope is a finite, reusable bridge on an allowed +side of a stage, with the scalar and native endpoints stated above. It does +not by itself cancel the full controller residual. The full compiler must +still lower the new routed accesses and odd division, bind the available +private array, prove all lifetime and recursive precision bounds, and add +the complete finite bill. A favourable rank count alone does not settle +those obligations. + +Reproduce from the workspace root: + +```sh +python3 -I -O -B work/centre-encoding-campaign-20261014/lanes/interface-proof/verify_bridge_operators.py --repo worktrees/k5-centre-sharing --interface work/centre-encoding-campaign-20261014/lanes/circuit-interface/INTERFACE.json --out work/centre-encoding-campaign-20261014/lanes/interface-proof/BRIDGE-OPERATOR-REVIEW.json +``` + +Expected status: `PASS_EXACT_BRIDGE_OPERATORS_AND_ACTUAL_LOCAL_GAUGE`. +All validation checks remain active under `-O`. The cover-algebra lane +supplied the bridge construction and phase formulas. This lane supplied +the independent operator binding, source replay, and one-accumulator bill. +The phase recipes and common-grid method are retained repository work. +This work used substantial OpenAI Codex assistance and independent agent +review. It is not independent human review. diff --git a/research/joint-query/evidence/CLEAN-J-CHECKS.json b/research/joint-query/evidence/CLEAN-J-CHECKS.json new file mode 100644 index 0000000000..c8ca09c4e9 --- /dev/null +++ b/research/joint-query/evidence/CLEAN-J-CHECKS.json @@ -0,0 +1,67 @@ +{ + "J_row_support": { + "52": 112 + }, + "R_column_support": { + "4": 112 + }, + "R_row_support": { + "56": 8 + }, + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "clean_program_payload_sha256": "fa60b4af013dd8b8db289845e3ed597720ff955751ad270c3d58236b64080877", + "geometry": { + "axes": 9, + "helpers": 480, + "ports": 112 + }, + "orientations": { + "backward": { + "canonical_scalar_frames": "PASS", + "child_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "child_rank_mass": 5522, + "correction_adds": 580, + "correction_clears": 16, + "independent_input_columns": 712, + "missing_clear_control": "REJECT", + "missing_correction_control": "REJECT", + "persistent_helpers_restored": 480, + "persistent_native_events": 5056, + "primitive_bound_real_components": 202138, + "private_outputs_zero": 8, + "removed_centre_rank_mass": 64, + "scalar_macros": 20089 + }, + "forward": { + "canonical_scalar_frames": "PASS", + "child_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "child_rank_mass": 5522, + "correction_adds": 580, + "correction_clears": 16, + "independent_input_columns": 712, + "missing_clear_control": "REJECT", + "missing_correction_control": "REJECT", + "persistent_helpers_restored": 480, + "persistent_native_events": 5056, + "primitive_bound_real_components": 202138, + "private_outputs_zero": 8, + "removed_centre_rank_mass": 64, + "scalar_macros": 20089 + } + }, + "scope": "Exact scalar maps, canonical frame access and retained native events. Native recipe phases, global hosting and supplier admission are separate.", + "source_base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "status": "PASS_PINNED_CLEAN_J_RECONSTRUCTION" +} diff --git a/research/joint-query/evidence/CONSERVED-QQ16.json b/research/joint-query/evidence/CONSERVED-QQ16.json new file mode 100644 index 0000000000..7a155a27dc --- /dev/null +++ b/research/joint-query/evidence/CONSERVED-QQ16.json @@ -0,0 +1,428 @@ +{ + "B_cases": 28, + "F_cases": 9, + "complete_common_chart_input_columns_per_orientation": 712, + "controls": [ + "late A input read", + "early T query", + "early F source update", + "early F target copy", + "positive inverse replacement", + "omitted payload translation", + "payload-only owner route" + ], + "full_cover_map_inverse_orders": true, + "invoices": { + "B": { + "arbitrary_helpers": 480, + "arbitrary_private_inputs_discarded": 8, + "complete_scalar": { + "macros": 21401, + "operations": { + "add": 20654, + "clear": 32, + "scale": 715 + }, + "real_primitives": 214986 + }, + "existing_owned_C0_fields": 1, + "formal_prefix": { + "formal_prefix_ceiling_log2": 73, + "formal_triangle_Horner_bound": "573411134169296526275133/64" + }, + "native_mass": 5546, + "native_profile": { + "1": 2436, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "new_fields": 0, + "private_outputs_zero": 8 + }, + "F": { + "arbitrary_helpers": 480, + "arbitrary_private_inputs_discarded": 8, + "complete_scalar": { + "macros": 21025, + "operations": { + "add": 20278, + "clear": 32, + "scale": 715 + }, + "real_primitives": 211210 + }, + "existing_owned_C0_fields": 1, + "formal_prefix": { + "formal_prefix_ceiling_log2": 55, + "formal_triangle_Horner_bound": "5413950274051752469/256" + }, + "native_mass": 5530, + "native_profile": { + "1": 2420, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "new_fields": 0, + "private_outputs_zero": 8 + } + }, + "native_cases": { + "B_1_2": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 2, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_3": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 3, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_4": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 4, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_5": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 5, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_6": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 6, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_1_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 1 + }, + "B_2_3": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 3, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_2_4": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 4, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_2_5": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 5, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_2_6": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 6, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_2_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_2_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 2 + }, + "B_3_4": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 4, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 3 + }, + "B_3_5": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 5, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 3 + }, + "B_3_6": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 6, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 3 + }, + "B_3_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 3 + }, + "B_3_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 3 + }, + "B_4_5": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 5, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 4 + }, + "B_4_6": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 6, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 4 + }, + "B_4_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 4 + }, + "B_4_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 4 + }, + "B_5_6": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 6, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 5 + }, + "B_5_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 5 + }, + "B_5_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 5 + }, + "B_6_7": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 7, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 6 + }, + "B_6_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 6 + }, + "B_7_8": { + "added_rank1_children": 24, + "explicit_cover_maps": 528, + "future": 8, + "matching_phase_ADD_reads": 1288, + "native_wrapper_maps": 48, + "orientation": "B", + "stage": 7 + }, + "F_0": { + "added_rank1_children": 8, + "explicit_cover_maps": 0, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 0 + }, + "F_1": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 1 + }, + "F_2": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 2 + }, + "F_3": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 3 + }, + "F_4": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 4 + }, + "F_5": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 5 + }, + "F_6": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 6 + }, + "F_7": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 7 + }, + "F_8": { + "added_rank1_children": 8, + "explicit_cover_maps": 288, + "matching_phase_ADD_reads": 912, + "native_wrapper_maps": 16, + "orientation": "F", + "stage": 8 + } + }, + "native_kernel_columns": 16384, + "owner_route_negative_control": { + "correct_owner_view_output_at_I": 1, + "incorrect_payload_only_output_at_I": 0, + "owner_I_input": 0, + "owner_rho_input": 1, + "payload_address": 0 + }, + "payload_sha256": "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef", + "retained_core_frame_and_byte_checks": true, + "scalar_phase_controls": 32, + "scope": "Exact local full-cover operator words with explicit sweep order, native maps and phases, the inherited local core, and complete local scalar/native invoices. Global helper owners, controller closure, child hosting, precision, stream/address costs and the complete supplier invoice are not admitted here.", + "source_pins": { + "B_native_component": "d7f75b34a56fc7acfb582d3a133c3eb817a29584a1f7136896420138cc155b35", + "F_native_component": "232035827945f2c13e32b7ced955f222eb1f349f0b409326c83fea5847088b1a", + "base": "40fdf1ce79720f810729e2bb8db7470c648e67c91fc365cd632c72eb2bcce44a", + "bridge_proof": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3", + "bridge_review": "c905a19d70f34c435c5f5454c6190bbfb1ce4594b1513bf76156acf620d7c6fc", + "charts": "498d85807dd3032de01b5da72a67717f02ee0ecf068e8c47f67d4f21034cd896", + "cover_action": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb", + "pair_proof": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "pair_receipt": "1f32819591103ab323c69cf50cf6579b0e881e105ca4a93b48125d5b89214c31", + "phase_helper": "416d50a33dab69fea7c775ac6f747163073b077169754663d2e8db353e17c2d9", + "positive_lines": "500c09dfc1d27ffd107341adf4c3c6874ee2c84e1a8afad91d931ed9e88fd1d7", + "scalar": "6b8d647a8ce2ff86f39b1947d11cbcdfd0f366e90c2816ff6cca09d47c75869c", + "scalar_producer": "48b8d2cf81c4b8d50c3aa0dcfe75090862a53fbbf9d051fd6985604e6191ba20", + "scalar_receipt": "c9729d71890df17027c75b028c535ad3bd8dc11633812bae856f80c38c52a0a1" + }, + "status": "PASS_CONSERVED_QQ16_COMPLETE_LOCAL_WORDS" +} diff --git a/research/joint-query/evidence/CONSERVED-QQ16.md b/research/joint-query/evidence/CONSERVED-QQ16.md new file mode 100644 index 0000000000..4639583c1b --- /dev/null +++ b/research/joint-query/evidence/CONSERVED-QQ16.md @@ -0,0 +1,338 @@ +# Complete local query words with conserved selected sums + +This construction uses sixteen existing data ports to carry centre +queries through a forward or backward call. The forward word puts its +full current source query in eight completed X ports. It moves the old +selected X value to another eight X ports. The backward word puts a +future source query in eight Y ports and a current query, with an +explicit selected-input term, in eight completed X ports. Both words +preserve the logical X-plus-Y sum at each of the sixteen selected ports. +Both complete maps are invertible on arbitrary data inputs. + +The emitted backward word has scalar bound 214986 and native mass 5546. +It adds twenty-four rank-one children. The forward word has scalar bound +211210 and native mass 5530. It adds eight rank-one children. Each uses +one existing owned private field C0 and no new field. All 480 arbitrary +ordinary helper inputs are restored. The eight owned private input +values may be arbitrary; the words discard them and return zero. + +These are complete local full-cover operator words. The payload gives +the exact owner maps, payload translations, intrinsic line recipes, +scalar gates, sweep barriers, and retained local core. It is not a +complete supplier. Global owner placement for the new sweeps and +children, controller closure, stream and address costs, precision, and +recursive admission remain open. No complete kappa improvement is +claimed. Independent review of this full-word payload is pending. + +## Sources and field contract + +The literal payload is `CONSERVED-QQ16-PROGRAMS.json.gz`. Its decompressed +SHA256 is + + 2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef. + +`CONSERVED-QQ16.json` gives the complete producer receipt. The emitter +pins each consumed source. The main inputs are: + +- `../CENTRE-FREE-PROGRAMS.json.gz`: the complete reviewed clean-J core; +- `../../residual-syndrome/physical-algebra/CONSERVED-QQ16-SCALARS.json.gz`: + the two fixed scalar words; +- `../../cover-algebra/JOINT-QUERY-TRANSFER.md`: the ordered pair maps, + inverses, and conserved-sum extension; +- `../../coherent-port/QQ16-CONSERVED-COMPONENT.json` and + `../../coherent-port/QQ16-CONSERVED-FORWARD.json`: the intrinsic native + recipes and component frame checks; +- `../../coherent-port/QQ16-COVER-ACTION-ADDENDUM.md` and + `../../interface-proof/BRIDGE-REVIEW.md`: the exact cover action and + its relation to the retained local core. + +The field namespace is L0 through L703 and C0 through C7. X is L0 +through L111. Y is L112 through L223. L224 through L703 are the 480 +ordinary helper fields. The formal replay has all 712 input columns. +No assumption is made that an input data, helper, or private value is +zero. Only owned private fields may be cleared. C0 is returned to +zero in frame I after each target row, before it is used for the next +cover owner. C1 through C7 are not used by the new wrappers. The +retained core clears all eight private fields. + +The core has 25155 events in each orientation. This includes 20089 +scalar macros, 3486 recursive child events, 1090 adapters, 480 residual +adapters, and ten phase markers. The payload retains all these bytes. +Their scalar bound is 202138 and their native mass is 5522. The existing +local frame checker is rerun on the complete core in both orientations. + +## Exact logical maps + +Use the actual matrix R, K=R^T/4, and J=I-KR. Then RK=14I. Set + + A=[0,7,20,27,36,46,57,111], + T=[21,37,47,76,81,87,92,110]. + +The two minors satisfy R_A R_A^T=R_T R_T^T=4I. Their inverses are +R_A^T/4 and R_T^T/4. Let U be the remaining 96 ports. An injection +with subscript A, T, or U is zero outside that set. + +For a current chart s, let D_s be the actual port-diagonal cover +route. Use the normalized queries and injections + + R_s=R D_s, K_s=D_s^-1 K, + P_s=D_s^-1 iota_T R_T^-1, + ell_s=R_T pi_T D_s. + +Thus R_s P_s=ell_s P_s=I, K_(s,T)=P_s, and R_s K_(s,U)=12I. +For a future chart t>s set + + E_t=I+P_(t,A)(R_t-ell_(t,A)). + +This is a unit. Its added term has only A output rows and no A input +columns, so its square is zero. Its inverse has the opposite sign. + +For the backward word define + + u=E_t y, a=ell_s x, b=R_s u. + +The exact output is + + y'_A=u_A, + y'_U=y_U+K_(s,U)a, + y'_T=u_T-P_s(b+11a), + x'_U=x_U-y_U, + x'_A=x_A+y_A-u_A, + x'_T=P_s(b+12a). (1) + +Consequently + + R_s y'=a, + ell_(t,A)y'=R_t y, + ell_s x'=b+12a, + x'_p+y'_p=x_p+y_p for p in A union T. (2) + +The T target contains b+12a, not b alone. The future selected query +and the current full query are different operator-valued quantities. + +For an explicit inverse, put Z_s=K_(s,U)-12P_s and +H_s=I+Z_sR_s. Since R_sZ_s=0, H_s^-1=I-Z_sR_s. From x',y' compute + + a=R_s y', b=ell_s x'-12a, + v=H_s^-1y', u=v+P_s(b-a), y=E_t^-1u. + +Then restore x_U=x'_U+y_U, x_T=P_sa, and +x_A=x'_A+y'_A-y_A. These equations prove both inverse orders. +They do not establish that all inverse reads are free at the output +frames. + +For the forward word put f=R_s x. Its output is + + x'_U=x_U-K_(s,U)f, + x'_A=P_(s,A)ell_s x, + x'_T=P_s f, + y'_U=y_U+x'_U, + y'_S=x_S+y_S-x'_S, S=A union T. (3) + +In normalized source coordinates (z,a,c), where a=ell_(s,A)x and +c=ell_s x, this is + + (z,a,c) -> (w,c,f), + f=R_(s,U)z+a+c, w=z-K_(s,U)f. + +Its inverse is z=w+K_(s,U)f and +a=-R_(s,U)w-11f-c. The Y inverse follows directly from (3). +This proves invertibility and conservation of all sixteen selected +pair sums. The two orientations are companions, not inverse circuits. + +The proof in the pinned pair note uses ordered multiplication. It +does not require two chart routes to commute. The common-chart +712-column replay checks the emitted coefficient word. The ordered +proof extends that word to the actual full-cover routes. The two +claims are recorded separately. + +## Cover action and native phases + +At cover owner d, the operator C_(d q) is the inherited complex line + + C_q=(1+i)I/2+(1-i)T_q/2. + +It satisfies C_q^2=T_q and C_q^-1=T_q C_q. A negative line therefore +uses the inherited positive rank-one recipe with translation q fused +into its left wrapper. A canonical binary line subspace does not +specify this phase and is not used as a replacement. + +At a positive backward stage s, the physical input frames are + + X_p: F_(d U_(s-1)), + Y_p: F_(d U_(s-1)) C_(d q_p)^-1, + +where U_j=L+E_1+...+E_j. After either retained local core, the frames +are F_(d U_s) on X and F_(d U_s) C_(d q_p)^-1 on Y. + +For each port and positive chart v, the pinned involution rho_v(p) +fixes q_p and swaps the eight chart vectors in q_p-perp with E_v. +Let beta_p[i]=(weight(B_p[i])-1)/2 modulo two. The Y alignment uses + + delta_Y(v,p)=q_p XOR lift_v(beta_p). + +The completed-X alignment uses + + delta_X(v,p)=B_p beta_p XOR lift_v(beta_p). + +The actual full-array map is + + M(g,delta) f(d,z_1,...,z_lambda) + = f(d g,z_1 XOR d delta,...,z_lambda XOR d delta). (4) + +Here g=rho_v(p). The owner changes by right multiplication. The +payload has a separate translation on every tensor layer. Spectators +are unchanged. There is no amplitude phase in (4). The phase of the +native frame changes because its owner and its payload translation +change. The registry gives the complete 73-column owner matrix and +translation for every map used. + +For operator composition, + + (g,a)(h,b)=(g h,a XOR g b), + (g,a)^-1=(g^-1,g^-1 a). + +The emitter checks both inverse orders, including the translation. +It computes the full Z4 phase polynomial after every map and native +line. Every new scalar ADD is checked against exact equal phase +polynomials, not just equal binary ranks. For a selected source q +read in target p's frame, the map is A_v(p)^-1 A_v(q). + +During emission, an incorrect interpretation of rho as a payload +permutation in one fixed array was identified and rejected before +the payload was frozen. The accepted bridge proof distinguishes +the two actions. The receipt includes a direct witness: give owner I +the constant value zero and owner rho the constant value one. The +correct map reads one at owner I. A payload-only permutation still +reads zero. Independent owner inputs cannot be identified. + +Stage-zero F has a separate base case. All X fields already have +the same FULL9 frame, D_0=I, and the source scalar suffix needs no +alignment. Its A output copies still need the eight inverse lines. +No stage-zero Y alignment is inferred. + +## Literal sweeps and private lifetime + +Every `cover_map` event is the declared bijection (4). A `cover_sweep` +must finish over the full cover before the next event. It is not a +local operation that assumes the other owners have already changed. +The `private_sweep` body is different: for each owner, execute the +whole clear, form, native child, add, and clear sequence before the +next owner. This uses one C0 array, not a full-cover C0 bank. + +The backward order is: + +1. Apply inverse C_p to the eight X_T fields. +2. For each p in A, move its four selected X source cohorts by the + exact current paths. Run the private sweep that forms + original y_p-(K_(s,A)a)_p, applies positive C_p, and adds it to X_p. + Return C0 to zero/I, then undo all four source-cohort maps. +3. Align all Y fields to chart t. Complete the E_t source sweep and + undo that alignment. +4. Align Y and the normalized X_T fields to chart s. Complete the U + scatter sweep, the eight selected swaps, and the final T-query + sweep in that order. The final query reads the changed U fields. +5. Undo the current alignment and restore X_T with positive C_p. +6. Run the complete retained backward core in its existing embedding. + +The forward order is: + +1. Run the complete retained forward core. +2. Align all X fields to the current completed chart, except at + stage zero. Run all five source scalar blocks in the frozen + order, with a completion barrier after each block. Undo alignment. +3. For each p in A, move its four selected source cohorts into the + X_p frame. Form the correction from the changed source, apply + inverse C_p on C0, and add it to Y_p. Clear C0 to zero/I and undo + all source-cohort maps. + +Each aligned port is a bijective view of one complete data family. +Thus, for a fixed common owner, distinct local blocks have disjoint +physical field addresses. The local scalar dependencies are exact +within this view. The barriers make later reads use the completed +earlier update. A target copy reads only unchanged selected source +cohorts and the same-port source until its private body is complete. +The temporary source maps are undone before the next copy row. + +These facts define a valid full-cover operator sequence. They do not +assign the new recursive children to unused helper owners, prove that +all sweeps fit the retained controller's live intervals, or price the +address implementation. Those are separate supplier obligations. + +## Complete local invoice + +All scalar bounds use the retained complex-to-real primitive ledger. +The count includes all new CLEARs, ADDs, signs, and the complete core. +It excludes the separate monomial maps and recursive child costs. + +| Word | Added scalar bound | Complete scalar bound | Added rank-one children | Native mass | Added map bound | +|---|---:|---:|---:|---:|---:| +| Backward, positive s