diff --git a/research/staged544-joint-child-rank-interface/PROOF.md b/research/staged544-joint-child-rank-interface/PROOF.md new file mode 100644 index 0000000000..83e6007f81 --- /dev/null +++ b/research/staged544-joint-child-rank-interface/PROOF.md @@ -0,0 +1,119 @@ +# A source-bound rank interface discriminator + +Chris R / Clear1nsight with substantial OpenAI Codex assistance. Apache-2.0. + +## Actual group and the proposed transfer + +The two PR3945 providers at `91f81d131252db704f945891da1ea54e29d46b8b` +contain the same four frame climbs on helpers600,601,602,604 at zero-based +B936,B937,B938,B941. Each entrance is span(45), each destination is +span(409,80,40,5,2), and the charged dimension increase is4. +The source window includes native maps on564 and405 at936 and on565 at939. +They remain at their literal positions. The checker traces the complete A +prefix and the B prefix through941, including every intervening native frame +boundary. It also verifies that the future helper inputs are untouched in +this window. It does not emit a retimed provider or claim a full dirty replay. +The intervening cut is checked to write only target families; its centre +descents are temporary readouts under the retained BORROW-WORD contract and +do not change the persistent helper frames used by this trace. + +Gonzalo Mier's PR4031 at `87899f26ccceb36d32985eab59dbeb467d90825b` +checks an old selected gauge44 rank4 grouping and the valid matrix identity +diag(A1,...,A4)diag(B1,...,B4)=diag(A1B1,...,A4B4) for4-by4 matrices. +It explicitly waives physical layout, native interfaces, hosting and dirty +restoration. Its optimistic profile is a screen, not a physical supplier. +We test the additional implication needed to transfer that rank16 invoice +to the actual PR3945 group. This is not a rerun of its80-call census. + +## The inherited rank parameter counts Fourier axes + +The retained exact compiler `bw_adapters.py:S_of,wrapped_ok` identifies a +rank-r residual with L (C_[r] tensor I) R, for monomial L and R. Here +C_[r]=C tensor ... tensor C on r binary axes, where +C=((1+i)I+(1-i)X)/2. `clifford_exact.py:fourier,lower_child` implements this +precise convention. A rank4 child therefore has16 nonzero entries per row +and per column; it is not a4-by4 matrix-multiplication oracle. + +The actual residual S=T_U T_E^-1 for the named source frames acts on512 +complex coordinates. Using the credited PR3987 scalar Gaussian arithmetic, +the checker evaluates all512 basis columns exactly. Each row and column has +16 nonzero entries, all with squared magnitude1/16. This fresh local check +does not import or execute the original compiler. Its arithmetic engine is +reused and credited; the proof below is independent of an observed hash. + +## Monomial and arbitrary-dirty padding obstruction + +Let A be the direct sum of the four actual residuals. It acts on2048 +coordinates and every row has support16. The desired all-input contract, +with any additional borrowed coordinates restored, is A direct-sum I_D. +It has row-support multiset {16 repeated2048 times,1 repeated D times}. +An arbitrary invertible monomial matrix permutes coordinates and multiplies +them by nonzero scalars. Left and right multiplication by such matrices +preserves the multiset of row supports. This includes source native L/R, +arbitrary monomial routing and arbitrary placement of the dirty auxiliaries. +It does not matter whether those monomials are free or charged. + +A single inherited rank16 child C_[16] tensor I has65536 nonzero entries in +every active row. Even after enough dirty padding to match dimensions, its +row-support multiset cannot equal that of A direct-sum I_D. Thus no one-call +rank16 implementation of this group exists using only monomial pre/post +maps and auxiliary coordinates returned identically for every initial value. +The same argument excludes any rank r>4 in this one-call contract, including +rank12. Identity spectator coordinates within a child are different from +an identity direct-sum bank: C_[16] tensor I still has support65536 per row. + +The dimension obstruction already appears at the literal base instance: +four512-coordinate banks give2048 coordinates, whereas a rank16 child needs +at least65536. Adding63488 arbitrary dirty coordinates resolves only that +dimension mismatch; the support mismatch remains. Clean initialized +coordinates, projections, nonmonomial encoders, multiple child queries or +changed output contracts are outside this proof and need their own invoices. + +For a tensor-power lift f>=1 of the source convention, each bank has2^(9f) +coordinates and support2^(4f), while a purported rank16 child has support +2^(16f). Four banks add two selector bits, not twelve Fourier axes. Here f +means the number of tensor copies of each source axis, not linear spectator +multiplicity used in the separate finite-lattice implementation PR4017. +The executable verifies the source base instance f=1; the all-f statement +follows from tensor-product support multiplication, not sampled larger f. + +There is a valid free algebraic batching: I_4 tensor C_[4] tensor I_32, +with the inherited block-diagonal monomial wrappers. It processes four +banks with two spectator selector axes. Its active Fourier rank remains4. +Consequently rank16 pricing does not follow from that identity. + +## Exact optimistic allowance and the complete obligation ledger + +At the pinned PR3945 tariff endpoint kappa=1730663236534549309146/10^24, +write H_r=r^(1-kappa). Replacing four H4 by one H16 would save + + 0.038249447579079975271991 < 4 H4-H16 + < 0.038249447579079975271992. + +The executable encloses log2 by an atanh series with a rational remainder +and exp(-x) by odd/even Taylor truncations, using exact fractions throughout. +This is an allowance before every additional interface cost. With every +other bill and inventory fixed, one added positive-rank recursive child costs +at least H1=1, exceeding the allowance. This conditional budget does not +exclude compensating savings elsewhere, changed hosting, or a new model. + +| Obligation | Status in this result | +|---|---| +| Four source frame transitions and literal native ordering | Freshly checked on both immutable providers | +| Exact local native all-input maps |512 basis columns checked; source arithmetic credited | +| One rank16 child with monomial wrappers and arbitrary-dirty identity return |Proved impossible under the stated contract | +| Valid spectator batching |Algebraic identity; active rank remains4 | +| Optimistic4H4-H16 allowance |Exact rational enclosure, before extra charges | +| Physical gathering/routing and larger hosting |Unknown; not zero | +| Changed nonlinear/linear nonmonomial encoders and dirty compensation |Unknown; excluded from the obstruction | +| Supplier stock, precision, tape, complete owner realization and root |Inherited/unrun; no changed provider or kappa claimed | + +## Open next questions + +The useful changed premise is a genuine multi-query or nonmonomial encoding +that preserves the four arbitrary inputs, permits their actual consumers, +and restores every borrowed coordinate. Its first test should exhibit one +explicit map outside the row-support argument and explain how its complete +cost fits the0.03825 allowance or which separately credited cost disappears. +A larger zero-charge grouping or a matrix direct-sum identity alone cannot +answer that question. This route stops here; no larger census is justified. diff --git a/research/staged544-joint-child-rank-interface/README.md b/research/staged544-joint-child-rank-interface/README.md new file mode 100644 index 0000000000..34f04a6771 --- /dev/null +++ b/research/staged544-joint-child-rank-interface/README.md @@ -0,0 +1,49 @@ +# Joint-child rank interface on the staged544 source + +**Scoped obstruction and exact allowance; no new kappa.** + +Four actual PR3945 rank4 frame climbs share their entrance and destination. +Their direct sum has16 nonzero entries per row. A single inherited rank16 +child has65536, so arbitrary monomial gathering/wrappers and identically +returned arbitrary-dirty padding cannot turn one into the other. Rank counts +Fourier axes in this supplier; ordinary block-matrix multiplication uses a +different interface. Valid selector batching retains active rank4. + +This resolves one missing transfer boundary from Gonzalo Mier's explicitly +zero-charge PR4031 screen, without disputing its matrix identity or claiming +a general batching obstruction. At the pinned PR3945 endpoint the hypothetical +4H4-to-H16 saving is only0.038249447579079975271991–992 H1 units, before +all omitted costs. [PROOF.md](PROOF.md) states the contract, proof, cost-status +ledger and open next questions. [RESULT.json](RESULT.json) retains the source +group, native events, exact support and rational allowance. + +Run the read-only registered normal/optimized replay: + +```sh +python3 scripts/research_package.py --package research/staged544-joint-child-rank-interface +``` + +Direct `python3 -B research/staged544-joint-child-rank-interface/verify.py` +also works without Git. `--record` intentionally regenerates RESULT.json; +ordinary verification checks its equality without writes. Frozen input hashes +are authenticated before the scientific checks. Five positive/negative +mathematical controls distinguish spectator identity from active Fourier +axes and reject the rank12/rank16 padded substitutions. This is not a full +provider dirty-state or owner replay. + +## Open next questions + +Can a nonmonomial or multi-query encoding preserve all four actual inputs, +their consumers and arbitrary borrowed state within the complete allowance? +First exhibit the changed map and price each new operation and any offsetting +credit. Physical encoding and restoration remain unresolved. A larger +zero-charge census does not remove the support obstruction in this contract. + +Credit: Gonzalo Mier/PR4031 provides the motivating rank4 retimed screen; +Dugongue/PR3945 provides both staged544 words; PR3969 binds their owner-cost +interpretation; PR3987 supplies the retained exact Gaussian phase arithmetic +and native compiler snapshots. The native code credits DreamingOfClouds, +chafreaky/PR458, PR2226 and its retained source lineage. Preserve the source +notices in frozen files. New proof/checker: Chris R / Clear1nsight with +substantial OpenAI Codex assistance. Apache-2.0. No independent human or +proof-assistant verification is claimed. diff --git a/research/staged544-joint-child-rank-interface/RESULT.json b/research/staged544-joint-child-rank-interface/RESULT.json new file mode 100644 index 0000000000..e182e7ab82 --- /dev/null +++ b/research/staged544-joint-child-rank-interface/RESULT.json @@ -0,0 +1,733 @@ +{ + "budget": { + "allowance": "4 H4 - H16", + "definition": "H_r=r^(1-kappa)", + "denominator": 1000000000000000000000000, + "kappa": "865331618267274654573/500000000000000000000000", + "lower_numerator": 38249447579079975271991, + "one_extra_H1_exceeds_allowance": true, + "upper_numerator": 38249447579079975271992 + }, + "controls": [ + "spectator-direct-sum positive", + "rank16 monomial/dirty-padding negative", + "rank12 monomial/dirty-padding negative", + "two-axis exact tensor versus selector negative", + "actual source frame contraction negative" + ], + "native": { + "column_support": { + "16": 512 + }, + "columns": 512, + "raw_gaussian_digest": "cceea321d198e93bc236fd1d3d95a0a98f52e27617ade2596ef4fe8557a19214", + "row_support": { + "16": 512 + } + }, + "new_kappa": false, + "providers": { + "base": { + "calls": [ + { + "index": 936, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 600 + }, + { + "index": 937, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 601 + }, + { + "index": 938, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 602 + }, + { + "index": 941, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 604 + } + ], + "native_events_preserved": [ + { + "columns": [ + 2, + 1, + 8, + 16, + 128, + 29, + 160, + 81, + 408 + ], + "entrance": [ + 258, + 130, + 84, + 44, + 1 + ], + "index": 936, + "register": 564, + "terminal": [ + 409, + 80, + 40, + 5, + 2 + ] + }, + { + "columns": [ + 1, + 8, + 16, + 128, + 256, + 147, + 140, + 169, + 209 + ], + "entrance": [ + 265, + 137, + 75, + 45 + ], + "index": 936, + "register": 405, + "terminal": [ + 80, + 40, + 5, + 2 + ] + }, + { + "columns": [ + 1, + 8, + 16, + 128, + 155, + 148, + 160, + 88, + 401 + ], + "entrance": [ + 258, + 130, + 74, + 45, + 31 + ], + "index": 939, + "register": 565, + "terminal": [ + 409, + 80, + 40, + 5, + 2 + ] + } + ], + "scalar_window": [ + [ + "add", + 600, + 564, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 601, + 564, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 602, + 564, + 1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 600, + 565, + 1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 601, + 565, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 604, + 565, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ] + ], + "scope": "Source chronology and disjoint-future-input check; no provider rewrite" + }, + "extra": { + "calls": [ + { + "index": 936, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 600 + }, + { + "index": 937, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 601 + }, + { + "index": 938, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 602 + }, + { + "index": 941, + "new": [ + 0, + 2, + 5, + 7, + 40, + 42, + 45, + 47, + 80, + 82, + 85, + 87, + 120, + 122, + 125, + 127, + 409, + 411, + 412, + 414, + 433, + 435, + 436, + 438, + 457, + 459, + 460, + 462, + 481, + 483, + 484, + 486 + ], + "old": [ + 0, + 45 + ], + "rank": 4, + "register": 604 + } + ], + "native_events_preserved": [ + { + "columns": [ + 2, + 1, + 8, + 16, + 128, + 29, + 160, + 81, + 408 + ], + "entrance": [ + 258, + 130, + 84, + 44, + 1 + ], + "index": 936, + "register": 564, + "terminal": [ + 409, + 80, + 40, + 5, + 2 + ] + }, + { + "columns": [ + 1, + 8, + 16, + 128, + 256, + 147, + 140, + 169, + 209 + ], + "entrance": [ + 265, + 137, + 75, + 45 + ], + "index": 936, + "register": 405, + "terminal": [ + 80, + 40, + 5, + 2 + ] + }, + { + "columns": [ + 1, + 8, + 16, + 128, + 155, + 148, + 160, + 88, + 401 + ], + "entrance": [ + 258, + 130, + 74, + 45, + 31 + ], + "index": 939, + "register": 565, + "terminal": [ + 409, + 80, + 40, + 5, + 2 + ] + } + ], + "scalar_window": [ + [ + "add", + 600, + 564, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 601, + 564, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 602, + 564, + 1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 600, + 565, + 1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 601, + 565, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + [ + "add", + 604, + 565, + -1, + 1, + [ + 409, + 80, + 40, + 5, + 2 + ] + ] + ], + "scope": "Source chronology and disjoint-future-input check; no provider rewrite" + } + }, + "status": "PASS_JOINT_CHILD_INTERFACE_DISCRIMINATOR", + "whole_provider_dirty_replay": false +} diff --git a/research/staged544-joint-child-rank-interface/SOURCES.json b/research/staged544-joint-child-rank-interface/SOURCES.json new file mode 100644 index 0000000000..42eede795a --- /dev/null +++ b/research/staged544-joint-child-rank-interface/SOURCES.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "snapshots": [ + { + "local": "frozen/WORD-base.json.gz", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "source_path": "research/staged544-terminal-gap-fill/owner/inputs/WORD-base.json.gz", + "bytes": 74428, + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "git_blob": "806784bf99d9d15004d2d227d06268556a0726c8" + }, + { + "local": "frozen/WORD-extra.json.gz", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "91f81d131252db704f945891da1ea54e29d46b8b", + "source_path": "research/staged544-terminal-gap-fill/owner/inputs/WORD-extra.json.gz", + "bytes": 74425, + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "git_blob": "c531be7383ad3ba941600c7ced14e5e10d6d1c67" + }, + { + "local": "frozen/exact_phase.py", + "source_path": "research/staged544-native-quadratic-audit/exact_phase.py", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "fc536202fdaa924158789a5ef59ac079bbe21922", + "bytes": 6557, + "sha256": "e3d76b3373ff40a83a4b212b3fe1c0b431b3cfdc807da601d6e7f273c02c6d30", + "git_blob": "4659b91e1b997a22e98a8631947aa79193fcf96f" + }, + { + "local": "frozen/bw_adapters.py", + "source_path": "research/staged544-native-quadratic-audit/vendor/bw_adapters.py", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "fc536202fdaa924158789a5ef59ac079bbe21922", + "bytes": 13755, + "sha256": "c5907050a9a7fa36d4fcba3ad4fe440d1bec2063360c095013891785ba65c3ce", + "git_blob": "82beaa9c1d13bcd5f79d0a5e10e8a10733eac347" + }, + { + "local": "frozen/clifford_exact.py", + "source_path": "research/staged544-native-quadratic-audit/vendor/clifford_exact.py", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "fc536202fdaa924158789a5ef59ac079bbe21922", + "bytes": 6824, + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2" + }, + { + "local": "frozen/PR4031-verify.py", + "source_path": "research/complex-rank4-retimed-blocks/verify.py", + "source_repository": "Gonzalo-Mier/integer-mult-bounds", + "source_commit": "87899f26ccceb36d32985eab59dbeb467d90825b", + "bytes": 14905, + "sha256": "db4b7c74f607ba4b97eb3fec0b7238449d0be3d2938f91916122ee676a720d35", + "git_blob": "9cc113d7df2f1c7dd3a9f3bc9c2e0871865aa2db" + }, + { + "local": "frozen/SOURCE-CREDITS.md", + "source_path": "research/staged544-native-quadratic-audit/SOURCE-CREDITS.md", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_commit": "fc536202fdaa924158789a5ef59ac079bbe21922", + "bytes": 2882, + "sha256": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "git_blob": "c054fad87eeaa510865e682ee0c976c4cd728da2" + } + ] +} diff --git a/research/staged544-joint-child-rank-interface/TASK.json b/research/staged544-joint-child-rank-interface/TASK.json new file mode 100644 index 0000000000..9bf51afe8c --- /dev/null +++ b/research/staged544-joint-child-rank-interface/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "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": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "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": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "actual_scope": "One source-bound PR3945 rank4 group; discriminate rank16 direct-sum transfer under monomial wrappers and arbitrary-dirty identity return.", + "scope_change_reason": "Explicitly assigned current-source combination of PR4031 screen with PR3945 native contract; resolve missing physical rank interface before construction.", + "bottleneck_link": "Larger child pricing only applies when the actual inherited Fourier-axis interface is implemented.", + "budget_minutes": 45, + "stop_rule": "Stop at source-bound support discriminator and exact allowance; no larger census.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json", + "author": "Chris R / Clear1nsight", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Can a nonmonomial or multi-query encoding meet the actual four-input, consumer and dirty-return contract within the full allowance?", + "why_it_matters": "Monomial one-child transfer is ruled out; arithmetic profile combination is insufficient.", + "first_step": "Exhibit one explicit nonmonomial map and every charged operation, including any compensating credit.", + "blocked_by": "Physical encoding, restoration and full invoice are unknown." + } + ], + "overlap": { + "root_cache": "research-round4-coordination/overlap-entry-cache.json", + "open_pr_bodies": 733, + "discussion_coverage": "Root partial live1166 read; not exhaustive", + "nearest": [ + "4031", + "3969", + "3987", + "4017" + ], + "novelty_claim": false + }, + "expansion_decision": "Narrow to one missing interface implication; stop without a supplier." +} diff --git a/research/staged544-joint-child-rank-interface/VERIFY.json b/research/staged544-joint-child-rank-interface/VERIFY.json new file mode 100644 index 0000000000..309abd26ca --- /dev/null +++ b/research/staged544-joint-child-rank-interface/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Both source groups, exact all-column residual, support obstruction, rational budget and controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Same production verification with assertions disabled." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/check_controls.py" + ], + "timeout_seconds": 90, + "checks": "Source corruption and stale retained rank reject through actual normal and optimized CLI." + } + ] +} diff --git a/research/staged544-joint-child-rank-interface/check_controls.py b/research/staged544-joint-child-rank-interface/check_controls.py new file mode 100644 index 0000000000..927f515171 --- /dev/null +++ b/research/staged544-joint-child-rank-interface/check_controls.py @@ -0,0 +1,24 @@ +"""Production-CLI rejecting controls, Apache-2.0, Chris R with OpenAI Codex.""" +from pathlib import Path +import tempfile,shutil,subprocess,sys,json +P=Path(__file__).resolve().parent + +def need(ok,why): + if not ok:raise ValueError(why) + +def main(): + for optimized in (False,True): + for mutation in ('source-byte','retained-rank'): + with tempfile.TemporaryDirectory(prefix='joint-child-control-') as tmp: + dst=Path(tmp)/'package';shutil.copytree(P,dst,ignore=shutil.ignore_patterns('__pycache__')) + if mutation=='source-byte': + f=dst/'frozen/WORD-base.json.gz';f.chmod(0o644);d=bytearray(f.read_bytes());d[-1]^=1;f.write_bytes(d) + expected='frozen source changed' + else: + f=dst/'RESULT.json';f.chmod(0o644);j=json.loads(f.read_text());j['providers']['base']['calls'][0]['rank']=16;f.write_text(json.dumps(j));expected='retained result differs' + argv=[sys.executable]+(['-O'] if optimized else [])+['-B',str(dst/'verify.py')] + p=subprocess.run(argv,capture_output=True,text=True,timeout=90) + need(p.returncode!=0 and expected in p.stderr,'production mutation accepted or wrong reason') + print('PASS_PRODUCTION_CLI_CONTROLS: source corruption and stale rank receipt reject in normal/optimized Python') + +if __name__=='__main__':main() diff --git a/research/staged544-joint-child-rank-interface/frozen/PR4031-verify.py b/research/staged544-joint-child-rank-interface/frozen/PR4031-verify.py new file mode 100644 index 0000000000..9cc113d7df --- /dev/null +++ b/research/staged544-joint-child-rank-interface/frozen/PR4031-verify.py @@ -0,0 +1,335 @@ +#!/usr/bin/env python3 +"""Verify a scoped rank-4 block-retiming screen on the pinned gauge44 trace.""" + +from collections import Counter, defaultdict +from decimal import Decimal, localcontext +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys +import tarfile + + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +ARCHIVE = ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz" +MEMBER = "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz" +CANONICAL_MEMBER = "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz" +ARCHIVE_SHA256 = "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" +PROGRAM_SHA256 = "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a" +WORD_SHA256 = "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" +EXPECTED_PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +EXPECTED_TARGETS = { + **{frame: 7 for frame in range(415, 423)}, + 431: 4, 432: 4, 433: 4, 434: 4, 436: 4, 437: 4, +} +MODEL = (73, 896, 9, 64) +GRID = Q(1, 10**13) + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def read_json_gzip(raw): + return json.loads(gzip.decompress(raw)) + + +def lregisters(operation): + """Return the L-registers read or written by a local scalar macro.""" + require(operation[0] == "add", f"unexpected retimed scalar macro: {operation}") + require(operation[1][0] == "L" and operation[2][0] == "L", + f"rank-4 retiming is not confined to L registers: {operation}") + return {operation[1][1], operation[2][1]} + + +def linear_state(events): + """Symbolically execute child outputs and rational ADDs on arbitrary L state.""" + state = {} + + def get(reg): + return state.get(reg, {f"x{reg}": Q(1)}) + + def add_scaled(left, right, scale): + out = dict(left) + for symbol, coefficient in right.items(): + out[symbol] = out.get(symbol, Q(0)) + scale * coefficient + if out[symbol] == 0: + del out[symbol] + return out + + for position, event in enumerate(events): + if event[0] == "climb": + reg = event[2] + state[reg] = {f"q{id(event)}": Q(1)} + else: + require(event[0] == "scalar", f"unexpected event in block window: {event}") + operation = event[1] + lregisters(operation) + destination, source = operation[1][1], operation[2][1] + scale = Q(operation[3], operation[4]) + state[destination] = add_scaled(get(destination), get(source), scale) + return state + + +def verify_batch(events, call_indices, block_side): + """Check a zero-charge retiming and the linear context around a block.""" + calls = [events[index] for index in call_indices] + require(len(calls) in (3, 4), "a block must contain three or four rank-4 calls") + require(all(call[0] == "climb" and call[-1] == 4 for call in calls), + "a block contains a non-rank-4 child") + require(len({call[1] for call in calls}) == 1, "mixed operand phase in one block") + require(len({call[4] for call in calls}) == 1, "mixed target frame in one block") + registers = [call[2] for call in calls] + require(len(set(registers)) == len(registers), "block child outputs alias") + require(sum(call[-1] for call in calls) == block_side, "wrong direct-sum side") + + lo, hi = call_indices[0], call_indices[-1] + interval = events[lo:hi + 1] + interval_calls = [lo + j for j, event in enumerate(interval) if event[0] == "climb"] + require(interval_calls == call_indices, "another child occurs inside the proposed block") + for event in interval: + if event[0] == "scalar": + lregisters(event[1]) + else: + require(event[0] == "climb", f"non-scalar event inside block: {event}") + + # A scalar reference to a later child register would observe a different value + # after the calls are moved before the ADDs. Exclude every such hazard. + for position in range(lo, hi + 1): + event = events[position] + if event[0] != "scalar": + continue + future = {call[2] for call_index, call in zip(call_indices, calls) + if call_index > position} + require(not (lregisters(event[1]) & future), + f"retiming changes a future child's input at event {position}") + + original = interval + retimed = [events[index] for index in call_indices] + retimed.extend(event for event in interval if event[0] == "scalar") + require(linear_state(original) == linear_state(retimed), + "moving the ADDs after independent child calls changes the exact linear map") + return { + "target_frame": calls[0][4], + "phase": calls[0][1], + "source_frames": [call[3] for call in calls], + "output_registers": registers, + "event_interval": [lo, hi], + "retimed_scalar_events": sum(event[0] == "scalar" for event in interval), + "block_side": block_side, + } + + +def verify_direct_sum_identity(blocks): + """Exhaustively compare all entries in diag(A_i)diag(B_i).""" + side = 4 * blocks + + def matrix_entry(operand, row, column): + if row // 4 != column // 4: + return None + return f"{operand}{row // 4}_{row % 4}_{column % 4}" + + for row in range(side): + for column in range(side): + actual = Counter() + for inner in range(side): + left = matrix_entry("a", row, inner) + right = matrix_entry("b", inner, column) + if left is not None and right is not None: + actual[(left, right)] += 1 + expected = Counter() + if row // 4 == column // 4: + block = row // 4 + for inner in range(4): + expected[(f"a{block}_{row % 4}_{inner}", + f"b{block}_{inner}_{column % 4}")] += 1 + require(actual == expected, + f"block-diagonal multiplication identity failed at {(row, column)}") + + +def decimal(q): + with localcontext() as context: + context.prec = 30 + return str(Decimal(q.numerator) / Decimal(q.denominator)) + + +def as_profile(counter): + return {str(rank): counter[rank] for rank in sorted(counter) if counter[rank]} + + +def ceiling(profile): + sys.path.insert(0, str(ROOT / "research/complex-local-word-ceiling")) + import ceiling as engine + return engine.ceiling(profile, *MODEL, grid=GRID)[1] + + +def main(write=False): + archive_bytes = ARCHIVE.read_bytes() + require(hashlib.sha256(archive_bytes).hexdigest() == ARCHIVE_SHA256, + "selected replay archive SHA-256 mismatch") + with tarfile.open(ARCHIVE, "r:gz") as archive: + program_bytes = archive.extractfile(MEMBER).read() + word_bytes = archive.extractfile(CANONICAL_MEMBER).read() + require(hashlib.sha256(program_bytes).hexdigest() == PROGRAM_SHA256, + "local program member SHA-256 mismatch") + require(hashlib.sha256(word_bytes).hexdigest() == WORD_SHA256, + "canonical word member SHA-256 mismatch") + + programs = read_json_gzip(program_bytes) + canonical = read_json_gzip(word_bytes) + selected_profile = {int(rank): int(count) + for rank, count in canonical["local_profile"].items()} + require(selected_profile == EXPECTED_PROFILE, "canonical local profile changed") + require(sum(rank * count for rank, count in selected_profile.items()) == 5586, + "selected paid rank mass changed") + + orientation_results = {} + first_orientation_batches = None + for orientation in ("forward", "backward"): + events = programs[orientation] + profile = Counter(event[-1] for event in events + if event[0] == "climb" or event[0] == "center") + require(dict(profile) == EXPECTED_PROFILE, + f"{orientation} event profile differs from the pinned word") + + by_target = defaultdict(list) + for index, event in enumerate(events): + if event[0] == "climb" and event[-1] == 4: + by_target[event[4]].append(index) + eligible = {frame: indices for frame, indices in by_target.items() + if len(indices) >= 4} + require({frame: len(indices) for frame, indices in eligible.items()} == EXPECTED_TARGETS, + f"{orientation} rank-4 target-frame census changed") + + batches = [] + for frame in sorted(eligible): + indices = eligible[frame] + sizes = [4, 3] if len(indices) == 7 else [4] + offset = 0 + for size in sizes: + chunk = indices[offset:offset + size] + offset += size + batches.append(verify_batch(events, chunk, size * 4)) + require(offset == len(indices), "target-frame calls were not fully partitioned") + require(len(batches) == 22, "unexpected number of direct-sum blocks") + require(Counter(batch["block_side"] for batch in batches) == {12: 8, 16: 14}, + "unexpected block-side distribution") + if first_orientation_batches is None: + first_orientation_batches = batches + else: + require(batches == first_orientation_batches, + "forward and backward retiming schedules differ") + orientation_results[orientation] = { + "rank4_calls": profile[4], + "eligible_target_frames": {str(frame): len(indices) + for frame, indices in sorted(eligible.items())}, + "blocks": len(batches), + "grouped_calls": sum(len(batch["output_registers"]) for batch in batches), + "grouped_rank_mass": sum(batch["block_side"] for batch in batches), + "block_sides": {str(side): count for side, count in + sorted(Counter(batch["block_side"] for batch in batches).items())}, + "retimed_scalar_events": sum(batch["retimed_scalar_events"] for batch in batches), + } + + verify_direct_sum_identity(3) + verify_direct_sum_identity(4) + + candidate = dict(selected_profile) + candidate[4] -= 80 + candidate[12] = candidate.get(12, 0) + 8 + candidate[16] = candidate.get(16, 0) + 14 + require(candidate[4] == 62, "candidate rank-4 count mismatch") + require(sum(rank * count for rank, count in candidate.items()) == 5586, + "rank-4 fusion changed paid rank mass") + + mixed_result = json.loads((ROOT / "research/complex-mixed-rank-diagonal-seed8433/RESULT.json") + .read_text()) + mixed_profile = {int(rank): int(count) + for rank, count in mixed_result["selected_profile"].items()} + require(sum(rank * count for rank, count in mixed_profile.items()) == 5586, + "pinned rank-2/3 profile does not preserve selected mass") + require(mixed_profile.get(4, 0) >= 80, + "rank-2/3 comparison profile lacks disjoint rank-4 calls") + combined = dict(mixed_profile) + combined[4] -= 80 + combined[12] = combined.get(12, 0) + 8 + combined[16] = combined.get(16, 0) + 14 + require(sum(rank * count for rank, count in combined.items()) == 5586, + "composed zero-charge profile changes paid mass") + + baseline_hi = ceiling(selected_profile) + candidate_hi = ceiling(candidate) + mixed_hi = ceiling(mixed_profile) + combined_hi = ceiling(combined) + kappa = lambda alpha: alpha / (1 + alpha) + result = { + "status": "PASS_COMPLEX_RANK4_RETIMED_BLOCKS", + "source": { + "archive_sha256": ARCHIVE_SHA256, + "local_program_sha256": PROGRAM_SHA256, + "canonical_word_sha256": WORD_SHA256, + "selected_profile": as_profile(Counter(selected_profile)), + }, + "per_orientation": orientation_results, + "direct_sum_identity": { + "tested_block_counts": [3, 4], + "child_side_4_to_block_side": {"3": 12, "4": 16}, + "identity": "diag(A_1,...,A_t) diag(B_1,...,B_t) = diag(A_1 B_1,...,A_t B_t)", + }, + "rank4_candidate": { + "grouped_calls": 80, + "new_blocks": {"12": 8, "16": 14}, + "profile": as_profile(Counter(candidate)), + "rank_mass": 5586, + "charges_waived": [ + "physical input gathering and block-diagonal layout", + "output routing and storage", + "frame/interface conversion", + "hosting and precision", + "arbitrary-dirty restoration", + ], + "ceiling_a_hi": str(candidate_hi), + "kappa_cap_hi": str(kappa(candidate_hi)), + "ceiling_gain_percent_over_selected": decimal(100 * (candidate_hi / baseline_hi - 1)), + "five_percent_gate_passed_alone": candidate_hi >= baseline_hi * Q(105, 100), + }, + "joint_zero_charge_screen": { + "predecessor": "research/complex-mixed-rank-diagonal-seed8433/RESULT.json", + "predecessor_profile": as_profile(Counter(mixed_profile)), + "composed_profile": as_profile(Counter(combined)), + "composed_ceiling_a_hi": str(combined_hi), + "composed_kappa_cap_hi": str(kappa(combined_hi)), + "ceiling_gain_percent_over_selected": decimal(100 * (combined_hi / baseline_hi - 1)), + "five_percent_gate_passed_under_zero_charge_only": combined_hi >= baseline_hi * Q(105, 100), + "new_supplier_or_kappa": False, + }, + "baseline_ceiling_a_hi": str(baseline_hi), + "mixed_rank23_ceiling_a_hi": str(mixed_hi), + "scope_wall": "The frozen trace authenticates child ranks, target frames and scalar register context, but does not specify a physical block-input/output ownership contract or complete gathering, routing, hosting, precision and dirty-restoration bill for a fused rank-12/rank-16 call.", + } + + result_path = PACKAGE / "RESULT.json" + if write: + result_path.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + else: + recorded = json.loads(result_path.read_text(encoding="utf-8")) + require(recorded == result, "RESULT.json differs from the independently recomputed screen") + + print("PASS_COMPLEX_RANK4_RETIMED_BLOCKS") + print(json.dumps({ + "forward_backward_batches": len(first_orientation_batches), + "grouped_calls": 80, + "new_block_sides": {"12": 8, "16": 14}, + "candidate_ceiling_a_hi": str(candidate_hi), + "combined_zero_charge_ceiling_a_hi": str(combined_hi), + "combined_five_percent_gate": result["joint_zero_charge_screen"]["five_percent_gate_passed_under_zero_charge_only"], + "new_kappa": False, + }, sort_keys=True)) + + +if __name__ == "__main__": + main(write="--write" in sys.argv[1:]) diff --git a/research/staged544-joint-child-rank-interface/frozen/SOURCE-CREDITS.md b/research/staged544-joint-child-rank-interface/frozen/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-joint-child-rank-interface/frozen/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-joint-child-rank-interface/frozen/WORD-base.json.gz b/research/staged544-joint-child-rank-interface/frozen/WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/staged544-joint-child-rank-interface/frozen/WORD-base.json.gz differ diff --git a/research/staged544-joint-child-rank-interface/frozen/WORD-extra.json.gz b/research/staged544-joint-child-rank-interface/frozen/WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/staged544-joint-child-rank-interface/frozen/WORD-extra.json.gz differ diff --git a/research/staged544-joint-child-rank-interface/frozen/bw_adapters.py b/research/staged544-joint-child-rank-interface/frozen/bw_adapters.py new file mode 100644 index 0000000000..82beaa9c1d --- /dev/null +++ b/research/staged544-joint-child-rank-interface/frozen/bw_adapters.py @@ -0,0 +1,165 @@ +"""Paid residual wrappers for entering helpers (Lemma A): generation and independent decoding. Apache-2.0. +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. The wrapper construction follows PR #458 +(chafreaky): a helper that starts at frame E and ends at FULL has the physical residual S_E = T_FULL T_E^-1 (apply T_E^-1 first); +S_E = L_E (C_[w] x I) R_E with R_E applied first; the wrappers R_E^-1 before the whole local invocation and L_E^-1 after its +full-frame cleanup turn the residual into the coordinate factor C_[w] x I and restore the other 9 - w coordinates identically. +usage: adapters_gk.py CANONICAL-WORD.json.gz RESIDUAL-ADAPTERS.json OUT-LEMMA-A.json +Writes the recipes (generation uses clifford_exact.lower_child) and then DECODES the serialized monomials with the primitive +constructors of clifford_exact (not lower_child) and checks, for every entrance frame, that L_E^-1 S_E R_E^-1 has exactly the +tableau and zero-state vector (global phase included) of fourier(9, range(w)); mutated recipes (wrong phase, swapped sides, wrong +translation, wrong width) must be rejected.""" +if not __debug__: + raise RuntimeError('assertions must remain enabled') # every check of this stage is an assert +import copy, gzip, json, sys +from pathlib import Path +# Package-path adaptation only; the exact wrapper mathematics is unchanged. +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / 'vendor/clifford')) # BW: the pinned vendor531 clifford_exact (byte copy) +sys.path.insert(0, str(HERE)) +from clifford_exact import canonical_frame, lower_child, fourier, diag, perm, xgate, Op, identity, transpose, inv, parity, monomial as mono_of, mv +import bw_gauss +n = 9; FULL = tuple(1 << i for i in range(n)) +def monomial_op(rec): + """decode a serialized monomial (matrix rows, quadratic rows, Z4 linear part, translation, phase)""" + out = diag(n, tuple(rec['quadratic_rows']), tuple(rec['linear_Z4'])).then(perm(n, tuple(rec['matrix_rows']))).then(xgate(n, rec['offset'])) + return out.then(Op(n, identity(n), [('phase', rec['phase'])])) +def S_of(U, END=FULL): + # HPE: a helper that starts at E=U and ends at END has residual T_END T_E^-1 (END = FULL is the inherited case) + return canonical_frame(n, tuple(U)).adjoint().then(canonical_frame(n, tuple(END))) +def wrapped_ok(U, rec, END=FULL): + """exactly: L^-1 S R^-1 = C_[w] x I (apply order: R^-1, S, L^-1), w = dim END - dim E""" + w = len(END) - len(U); S = S_of(U, END); Rm = monomial_op(rec['right']); Lm = monomial_op(rec['left']) + net = Rm.adjoint().then(S).then(Lm.adjoint()); target = fourier(n, range(w)) + return rec['rank'] == w and net.tab == target.tab and net.zero_state() == target.zero_state() +def _contains(a, b): + a = list(a) + for x in b: + for y in sorted(a, reverse=True): + if x >> (y.bit_length() - 1) & 1: x ^= y + if x: return False + return True +def Kop(G_cols): + """BW: K_G = perm(G) then diag(Q), Q = I + G^-T G^-1: PR2226's monomial() and the conjugator inside clifford_exact.canonical_frame.""" + G = transpose(tuple(G_cols), n); gi = inv(G, n) + Q = tuple((1 << i) ^ sum(parity(gi_i & gi_j) << j for j, gi_j in enumerate(transpose(gi, n))) for i, gi_i in enumerate(transpose(gi, n))) + return perm(n, G).then(diag(n, Q)) +def numeric_K(G_cols): + import numpy as np + pv, ph = bw_gauss.monomial(list(G_cols), n) + N = 1 << n; re = np.zeros((N, N), dtype=np.int64); im = np.zeros((N, N), dtype=np.int64) + unit = [(1, 0), (0, 1), (-1, 0), (0, -1)] + for x in range(N): re[pv[x], x], im[pv[x], x] = unit[ph[x]] + return re, im, 0 +def warp_ok(G_cols, rec): + """BW: the serialized monomial equals PR2226's exact numpy K_G on all 512 columns (indep. decode) and its op decodes to K_G exactly.""" + m = bw_gauss.recipe_matrix(rec, n) + if not bw_gauss.equal_scaled(numeric_K(G_cols), m): return False + dec = monomial_op(rec); ref = Kop(G_cols) + return dec.tab == ref.tab and dec.zero_state() == ref.zero_state() + +def main(): + c = json.load(gzip.open(sys.argv[1])); frames = c['frames']; v = c['v'] + starts = sorted({c['start'][r] for r in range(2 * v, len(c['start'])) if c['start'][r] != 0 and c['final'][r] == 1}) + # HPE: (entrance, terminal) pairs of helpers ending at a proper subspace; key 'E:U'. Inherited words have none. + ends = sorted({(c['start'][r], c['final'][r]) for r in range(2 * v, len(c['start'])) if c['final'][r] != 1}) + # COLD-HPE: e == 0 (a cold helper, entrance = bottom, T_0 = I) is allowed: the (0, U) recipe is keyed '0:U' + assert all(len(frames[u]) < n and _contains(frames[u], frames[e]) for e, u in ends) + cold_ends = [(e, u) for e, u in ends if e == 0] + recipes = {} + for f in starts: + U = frames[f]; rec, compiled = lower_child(S_of(U)) + recipes[str(f)] = dict(frame=f, vectors=list(U), entrance_rank=len(U), rank=rec['rank'], left=rec['left'], right=rec['right']) + for e, u in ends: + E, U = frames[e], frames[u]; rec, compiled = lower_child(S_of(E, U)) + recipes['%d:%d' % (e, u)] = dict(frame=e, terminal=u, vectors=list(E), terminal_vectors=list(U), entrance_rank=len(E), + terminal_rank=len(U), rank=rec['rank'], left=rec['left'], right=rec['right']) + # BW: monomial recipes of the warps K_G (anticipatory dirty borrowing, PR2226): one per operator, serialized like a wrapper monomial + warp_recipes = {} + for w in c.get('warps', []): + _, rec_k = mono_of(Kop(w['G_columns'])) + warp_recipes[str(w['op'])] = dict(op=w['op'], from_frame=w['from_frame'], to_frame=w['to_frame'], G_columns=list(w['G_columns']), K=rec_k) + Path(sys.argv[2]).write_text(json.dumps(dict(status='RESIDUAL_ADAPTER_RECIPES', recipes=recipes, warps=warp_recipes), sort_keys=True, separators=(',', ':')) + '\n') + # ---- independent decode of the serialized file + data_all = json.loads(Path(sys.argv[2]).read_text()); data = data_all['recipes'] + dot = lambda a, b: bin(a & b).count('1') & 1 + detail = [] + for f in starts: + rec = data[str(f)]; U = frames[f] + assert wrapped_ok(U, rec), ('wrapper product is not C_[w] x I', f) + detail.append(dict(frame=f, entrance_rank=len(U), residual_width=n - len(U), vectors=list(U), all_even_weight=all(bin(x).count('1') % 2 == 0 for x in U), + totally_isotropic=all(dot(a, b) == 0 for a in U for b in U))) + hdetail = [] + for e, u in ends: # HPE: independent decode, residual width = dim U - dim E + rec = data['%d:%d' % (e, u)]; E, U = frames[e], frames[u] + assert wrapped_ok(E, rec, U), ('HPE wrapper product is not C_[w] x I', e, u) + hdetail.append(dict(frame=e, terminal=u, entrance_rank=len(E), terminal_rank=len(U), residual_width=len(U) - len(E))) + controls = [] + def reject(name, fn): + f = starts[0]; rec = copy.deepcopy(data[str(f)]); fn(rec) + if wrapped_ok(frames[f], rec): raise AssertionError('mutated wrapper accepted: ' + name) + controls.append(name) + reject('wrong global phase', lambda r: r['right'].__setitem__('phase', (r['right']['phase'] + 1) % 4)) + reject('wrong translation', lambda r: r['left'].__setitem__('offset', r['left']['offset'] ^ 1)) + reject('wrong quadratic form', lambda r: r['right'].__setitem__('quadratic_rows', [x ^ 2 if i == 0 else x for i, x in enumerate(r['right']['quadratic_rows'])]) if False else r['right']['linear_Z4'].__setitem__(0, (r['right']['linear_Z4'][0] + 2) % 4)) + reject('sides swapped', lambda r: (r.__setitem__('left', r['right']), r.__setitem__('right', r['left']))) + reject('wrong width', lambda r: r.__setitem__('rank', r['rank'] + 1)) + if ends: # HPE controls on the first (E, U) pair + e, u = next((p for p in ends if p[0] != 0), ends[0]); rec0 = data['%d:%d' % (e, u)] # COLD-HPE: an entering pair if any (= ends[0] without cold ends) + def hreject(name, ok): + if ok: raise AssertionError('HPE mutation accepted: ' + name) + controls.append(name) + hreject('hpe: U-wrapper decoded against a FULL ending', wrapped_ok(frames[e], rec0)) + hreject('hpe: width misreported as 9 - dim E', wrapped_ok(frames[e], dict(rec0, rank=n - len(frames[e])), frames[u])) + other = next(f for f in range(len(frames)) if f != u and len(frames[f]) == len(frames[u]) and _contains(frames[f], frames[e])) + hreject('hpe: wrong terminal hyperplane', wrapped_ok(frames[e], rec0, frames[other])) + fe = next(((e2, u2) for e2, u2 in ends if str(e2) in data), None) + if fe: # an entrance shared with FULL-ended helpers: R_{E,FULL} must not serve as R_{E,U} + r2 = data['%d:%d' % fe] + hreject('hpe: pre wrapper resolved to the FULL recipe R_{E,FULL}', wrapped_ok(frames[fe[0]], dict(r2, right=data[str(fe[0])]['right']), frames[fe[1]])) + hreject('hpe: wrong global phase', wrapped_ok(frames[e], dict(rec0, left=dict(rec0['left'], phase=(rec0['left']['phase'] + 1) % 4)), frames[u])) + if cold_ends: # COLD-HPE controls on the first cold pair (0, U): factor_iff_pre says only R_{0,U} itself may precede + e, u = cold_ends[0]; recc = data['%d:%d' % (e, u)]; E, U = frames[e], frames[u] + ID = dict(matrix_rows=[1 << i for i in range(n)], offset=0, quadratic_rows=[0] * n, linear_Z4=[0] * n, phase=0) + assert monomial_op(ID).tab == identity(n) # the control's wrapper really is the identity + def creject(name, ok): + if ok: raise AssertionError('cold HPE mutation accepted: ' + name) + controls.append(name) + creject('cold hpe: identity pre wrapper instead of R_{0,U}', wrapped_ok(E, dict(recc, right=ID), U)) + creject('cold hpe: identity post wrapper instead of L_{0,U}', wrapped_ok(E, dict(recc, left=ID), U)) + creject('cold hpe: no wrappers (cold FULL convention L = R = I)', wrapped_ok(E, dict(recc, left=ID, right=ID), U)) + creject('cold hpe: U-wrapper decoded against a FULL ending', wrapped_ok(E, recc)) + creject('cold hpe: width misreported as 9', wrapped_ok(E, dict(recc, rank=n), U)) + other = next(f for f in range(len(frames)) if f != u and len(frames[f]) == len(frames[u])) + creject('cold hpe: wrong terminal hyperplane', wrapped_ok(E, recc, frames[other])) + creject('cold hpe: wrong global phase', wrapped_ok(E, dict(recc, right=dict(recc['right'], phase=(recc['right']['phase'] + 1) % 4)), U)) + ent = next((p for p in ends if p[0] != 0 and p[1] == u), None) + same = lambda x, y: monomial_op(x).tab == monomial_op(y).tab and monomial_op(x).zero_state() == monomial_op(y).zero_state() + if ent and not same(data['%d:%d' % ent]['right'], recc['right']): # an entering helper ending at the same U: its R_{E,U} must not serve as R_{0,U} + creject('cold hpe: pre wrapper resolved to an entering recipe R_{E,U}', wrapped_ok(E, dict(recc, right=data['%d:%d' % ent]['right']), U)) + wdetail = [] + for w in c.get('warps', []): # BW: independent decode of every warp recipe, then mutation controls on the first warp + rec = data_all['warps'][str(w['op'])] + assert rec['G_columns'] == w['G_columns'] + assert warp_ok(w['G_columns'], rec['K']), ('warp recipe differs from the exact monomial K_G', w['op']) + wdetail.append(dict(op=w['op'], from_frame=w['from_frame'], to_frame=w['to_frame'], columns_checked=1 << n)) + if c.get('warps'): + w0 = c['warps'][0]; k0 = data_all['warps'][str(w0['op'])]['K'] + def wreject(name, ok): + if ok: raise AssertionError('warp mutation accepted: ' + name) + controls.append(name) + wreject('warp: wrong global phase', warp_ok(w0['G_columns'], dict(k0, phase=(k0['phase'] + 1) % 4))) + wreject('warp: wrong translation', warp_ok(w0['G_columns'], dict(k0, offset=k0['offset'] ^ 1))) + wreject('warp: wrong linear phase', warp_ok(w0['G_columns'], dict(k0, linear_Z4=[(k0['linear_Z4'][0] + 2) % 4] + k0['linear_Z4'][1:]))) + wreject('warp: wrong quadratic form', warp_ok(w0['G_columns'], dict(k0, quadratic_rows=[k0['quadratic_rows'][0] ^ 2, k0['quadratic_rows'][1] ^ 1] + k0['quadratic_rows'][2:]))) + wreject('warp: recipe of another operator', warp_ok(w0['G_columns'], data_all['warps'][str(c['warps'][1]['op'])]['K'])) + wreject('warp: inverse recipe used as the warp', warp_ok(w0['G_columns'], mono_of(Kop(w0['G_columns']).adjoint())[1])) + G2 = list(w0['G_columns']); G2[0] ^= G2[1] + wreject('warp: wrong G (frame-changed column)', warp_ok(G2, k0)) + sing = list(w0['G_columns']); sing[1] = sing[0] + try: Kop(sing); raise SystemExit('non-invertible G accepted') + except (AssertionError, StopIteration, ValueError): controls.append('warp: non-invertible G') + res = dict(status='PASS_RESIDUAL_WRAPPERS_ARE_EXACT', frames=len(detail), **({'hyperplane_end_pairs': hdetail} if ends else {}), **({'cold_hyperplane_end_pairs': len(cold_ends)} if cold_ends else {}), wrappers_reject=controls, all_even_weight=all(d['all_even_weight'] for d in detail), **({'warp_recipes_exact_on_all_512_columns': wdetail} if wdetail else {}), + all_totally_isotropic=all(d['totally_isotropic'] for d in detail), detail=detail) + Path(sys.argv[3]).write_text(json.dumps(res, indent=1) + '\n') + print('Lemma A (exact): L^-1 S_E R^-1 = C_[w] x I for', len(detail), 'entrance frames, global phase included;', len(controls), 'wrapper mutations rejected; all-even-weight:', res['all_even_weight']) +if __name__ == '__main__': main() diff --git a/research/staged544-joint-child-rank-interface/frozen/clifford_exact.py b/research/staged544-joint-child-rank-interface/frozen/clifford_exact.py new file mode 100644 index 0000000000..166841a037 --- /dev/null +++ b/research/staged544-joint-child-rank-interface/frozen/clifford_exact.py @@ -0,0 +1,149 @@ +"""Small exact Gaussian-dyadic Clifford compiler, independent of gx internals. +Paulis use i^p X^x Z^z. State vectors use integer Gaussian numerators / 2^d. +The tableau is supplemented by a literal circuit, so global phases are kept. +""" +from dataclasses import dataclass + +def parity(x):return x.bit_count()&1 +def rank(rows): + p={} + for x in rows: + while x: + b=x.bit_length()-1 + if b not in p:p[b]=x;break + x^=p[b] + return len(p) +def transpose(rows,n):return tuple(sum(((rows[j]>>i)&1)<>j&1);a[j],a[k]=a[k],a[j] + for i in range(n): + if i!=j and a[i]>>j&1:a[i]^=a[j] + assert [r&((1<>n for r in a) +def basis_extend(cols,n): + out=[] + for x in list(cols)+[1<len(out):out.append(x) + assert len(out)==n + return tuple(out) +def nullspace(rows,n): + a=list(rows);p=[];k=0 + for j in range(n): + t=next((i for i in range(k,len(a)) if a[i]>>j&1),None) + if t is None:continue + a[t],a[k]=a[k],a[t] + for i in range(len(a)): + if i!=k and a[i]>>j&1:a[i]^=a[k] + p.append(j);k+=1 + return tuple((1<>j)&1)<>i&1:out=pmul(out,T[i]) + for i in range(n): + if z>>i&1:out=pmul(out,T[n+i]) + return out +def compose(A,B):return tuple(apply(A,p) for p in B) +def inverse(T): + n=len(T)//2;cols=[x|(z<>n;u,v,p=apply(T,(x,z,0));assert (u,v)==identity(n)[j][:2];out.append((x,z,(-p)%4)) + return tuple(out) +def qvalue(Q,alpha,x,n): + return (sum(alpha[i] for i in range(n) if x>>i&1)+2*sum(parity((Q[i]>>(i+1))&(x>>(i+1))) for i in range(n) if x>>i&1))%4 +def mul_i(a,p): + x,y=a;p%=4 + return [(x,y),(-y,x),(-x,-y),(y,-x)][p] +@dataclass +class Op: + n:int + tab:tuple + circuit:list + def then(self,b): + assert self.n==b.n + return Op(self.n,compose(b.tab,self.tab),self.circuit+b.circuit) + def adjoint(self): + circ=[] + for e in reversed(self.circuit): + if e[0]=='P':circ.append(('P',inv(e[1],self.n))) + elif e[0]=='D':circ.append(('D',e[1],tuple((-x)%4 for x in e[2]))) + elif e[0]=='C':circ.append(('C',e[1],-e[2])) + elif e[0]=='phase':circ.append(('phase',(-e[1])%4)) + else:circ.append(e) + return Op(self.n,inverse(self.tab),circ) + def zero_state(self,basis=0): + N=1<>i)&1 for i in range(n)) + assert all(alpha[i]%2==(Q[i]>>i)&1 for i in range(n)) + return Op(n,tuple([(1<>i&1 else 0,1<>i&1 else 0) for i in range(n)]),[('C',q,sgn)]) +def xgate(n,b):return Op(n,tuple([(1<>i)&1)) for i in range(n)]),[('X',b)]) +def fourier(n,axes=None): + out=ident(n) + for i in range(n) if axes is None else axes:out=out.then(cgate(n,1<len(selected):picks.append(j);selected.append(x) + assert len(picks)==r and all(x>>r==0 for x in Bcols) + Br=transpose(selected,r);Bi=inv(Br,r);Dr=transpose([Dcols[j]&((1<>i&1] + q.append((sum(gram[i][i] for i in bits)+2*sum(gram[i][j]for i in bits for j in bits if i>j)&1)==((quad[j]>>i)&1)for i in range(N)for j in range(N)),'symmetric quadratic form') + need(all(alpha[i]%2==((quad[i]>>i)&1)for i in range(N)),'quadratic parity') + perm=[];phasev=[] + for x in range(SIZE): + perm.append(sum(((r&x).bit_count()%2)<>i&1] + phasev.append((phase+sum(alpha[i]for i in bits)+2*sum((quad[i]>>j)&1 for i in bits for j in bits if i0 else 2]+=1 + elif not r:phase_hist[1 if s>0 else 3]+=1 + digest.update(json.dumps([x,da,sorted(a.items())],separators=(',',':')).encode()) + return dict(columns=SIZE,nonzero_coefficients=support,gaussian_axis_phase_histogram=phase_hist,operator_sha256=digest.hexdigest()) + +def lift_cocycle(G,H): + """K_H K_G = K_(HG) Z_ell. Exact finite Z4 phase defect.""" + gp,gq=kernel(tuple(G));hp,hq=kernel(tuple(H)) + HG=tuple(lin(H,c)for c in G);cp,cq=kernel(HG) + defect=[(gq[x]+hq[gp[x]]-cq[x])%4 for x in range(SIZE)] + ell=sum((defect[1<0 and n&(n-1)==0,'not a subspace size') + return n.bit_length()-1 + +REGS=(600,601,602,604) +POSITIONS=(936,937,938,941) +ENTRANCE=(45,) +TERMINAL=(409,80,40,5,2) + +def trace_group(w): + """Trace source frame state through literal A/B ordering; never retime native maps.""" + current={r:span([w['ports'][r]]) if r<112 else span([]) for r in range(704) if r not in w['removed']} + for r,b in w['start_extra'].items():current[int(r)]=span(b) + calls=[] + def gate(g,section,index): + if g[0]=='warp': + need(current[g[1]]==span(g[3]),'A warp entrance');current[g[1]]=span(g[4]);return + need(g[0] in ('add','scale'),'scalar kind') + for r in g[1:3] if g[0]=='add' else g[1:2]: + target=span(g[-1]);need(current[r]<=target,'scalar containment') + if section=='B' and r in REGS and index in POSITIONS: + calls.append(dict(register=r,index=index,old=sorted(current[r]),new=sorted(target),rank=dim(target)-dim(current[r]))) + current[r]=target + for i,g in enumerate(w['A']):gate(g,'A',i) + # The middle cut only writes target families. Its centre descents are + # temporary readouts, not persistent helper-frame updates (BORROW-WORD). + need(all(g[0]=='add' and 112<=g[1]<224 and g[-1] is None for g in w['cut']),'target-only cut contract') + native=[] + for i in range(max(POSITIONS)+1): + for pos,r,cols,u,e in w['warps']: + if pos==i: + need(current[r]==span(u),'B warp entrance');current[r]=span(e) + if min(POSITIONS)<=i<=max(POSITIONS):native.append(dict(index=i,register=r,entrance=u,terminal=e,columns=cols)) + gate(w['B'][i],'B',i) + positive=[x for x in calls if x['rank']] + need([(x['register'],x['index'],x['rank']) for x in positive]==list(zip(REGS,POSITIONS,[4]*4)),'actual group ranks') + need(all(set(x['old'])==set(span(ENTRANCE)) and set(x['new'])==set(span(TERMINAL)) for x in positive),'actual group frames') + need([(x['index'],x['register']) for x in native]==[(936,564),(936,405),(939,565)],'native ordering') + # A local dependency check only. No whole-word rewrite or dirty-state replay is claimed. + for call in positive: + for j in range(min(POSITIONS),call['index']): + g=w['B'][j] + touched=g[1:3] if g[0]=='add' else g[1:2] + need(call['register'] not in touched,'future call is touched early') + need(all(x['register']!=call['register'] for x in native if x['index']<=call['index']),'native touches future call') + return dict(calls=positive,native_events_preserved=native,scalar_window=w['B'][936:942],scope='Source chronology and disjoint-future-input check; no provider rewrite') + +def native_support(): + """All 512 columns of actual T_U T_E^-1, with exact Gaussian arithmetic.""" + columns=Counter();rows=Counter();digest=hashlib.sha256() + for x in range(512): + v,d0=phase.frame({x:(1,0)},ENTRANCE,True) + v,d1=phase.frame(v,TERMINAL) + columns[len(v)]+=1 + for y in v:rows[y]+=1 + need(all(Q(a*a+b*b,1<<(2*(d0+d1)))==Q(1,16) for a,b in v.values()),'residual entry magnitude') + digest.update(json.dumps([x,d0+d1,sorted(v.items())],separators=(',',':')).encode()) + need(columns=={16:512} and Counter(rows.values())=={16:512},'actual residual support') + return dict(columns=512,column_support={str(k):v for k,v in columns.items()},row_support={str(k):v for k,v in Counter(rows.values()).items()},raw_gaussian_digest=digest.hexdigest()) + +def budget(): + k=Q(1730663236534549309146,10**24) + z=Q(1,3);loglo=2*sum((z**(2*j+1)/Q(2*j+1) for j in range(60)),Q(0)) + loghi=loglo+2*z**121/(121*(1-z*z)) + def power2(exponent): + a,b=k*exponent*loglo,k*exponent*loghi + def expm(x,n):return sum(((-x)**i/Q(math.factorial(i)) for i in range(n+1)),Q(0)) + need(0