diff --git a/research/literal-positive-c-leaf/.gitignore b/research/literal-positive-c-leaf/.gitignore new file mode 100644 index 0000000000..0b099c6efc --- /dev/null +++ b/research/literal-positive-c-leaf/.gitignore @@ -0,0 +1,5 @@ +__pycache__/ +RESULT-OPT.json +SOURCE-GATE-OPT.json +BIG-RESULT-OPT.json +BIG-TIMING-OPT.txt diff --git a/research/literal-positive-c-leaf/BIG-RESULT.json b/research/literal-positive-c-leaf/BIG-RESULT.json new file mode 100644 index 0000000000..5141a181c2 --- /dev/null +++ b/research/literal-positive-c-leaf/BIG-RESULT.json @@ -0,0 +1,98 @@ +{ + "actual_f2": { + "accepted": true, + "data_writes": 2621440, + "exteriors_preserved": true, + "header_preserved": true, + "header_writes": 0, + "heads_returned": true, + "input_bits": 2621440, + "output_sha256": "d74e7771c2007ef7e2e49c43cade4ee0a72bfb2ac6e8f711671d88c27aac5216", + "private_blank": true, + "private_history": 13369462, + "shape": [ + 2, + 1, + 1, + 1, + 5, + 2 + ], + "steps": 704382528 + }, + "compiler_flags": [ + "-std=c++17", + "-O2" + ], + "controls": [ + "skip every axis after the first while preserving data length, owner, heads and private retirement" + ], + "f1_cross_interpreter": { + "accepted": true, + "data_writes": 3072, + "exteriors_preserved": true, + "header_preserved": true, + "header_writes": 0, + "heads_returned": true, + "input_bits": 3072, + "output_sha256": "598cc9a4e58b97ec53e8e9acf5bb1a11540656844a98fce6afc61fa2d57780ab", + "private_blank": true, + "private_history": 15965, + "shape": [ + 1, + 1, + 1, + 1, + 3, + 1 + ], + "steps": 514892 + }, + "f2_endpoint_only_reject": { + "accepted": false, + "data_writes": 0, + "exteriors_preserved": true, + "header_preserved": true, + "header_writes": 0, + "heads_returned": false, + "input_bits": 1048576, + "output_sha256": "951a3fc0fc429662a4f46c011dea531ee4b13f11cf6da97b5e83525daab4ebda", + "private_blank": false, + "private_history": 2752608, + "shape": [ + 2, + 1, + 1, + 1, + 2, + 2 + ], + "steps": 36898051 + }, + "f2_one_axis_mutant": { + "accepted": true, + "data_writes": 2621440, + "exteriors_preserved": true, + "header_preserved": true, + "header_writes": 0, + "heads_returned": true, + "input_bits": 2621440, + "output_sha256": "5dc2b69c5029846c0f93217a80419f1535749a54809dfd334bd2cec5e7d44701", + "private_blank": true, + "private_history": 10616950, + "shape": [ + 2, + 1, + 1, + 1, + 5, + 2 + ], + "steps": 401212870 + }, + "interpreter_sha256": "b6180d3b12f7bb9142c146c57a0e868a74d3d7e3653c7264fb890c57f85cc08b", + "program_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", + "scope": "Actual fixed m=9 table, complete 262144-address f=2 array; no reduced dimension or record subsampling.", + "status": "PASS_ACTUAL_M9_F2_LITERAL_C", + "table_sha256": "ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9" +} diff --git a/research/literal-positive-c-leaf/BIG-TIMING.txt b/research/literal-positive-c-leaf/BIG-TIMING.txt new file mode 100644 index 0000000000..a049c0a4a2 --- /dev/null +++ b/research/literal-positive-c-leaf/BIG-TIMING.txt @@ -0,0 +1 @@ +Wall seconds f1/full-f2/mutant/endpoint-reject: 0.011 6.818 4.364 0.305 diff --git a/research/literal-positive-c-leaf/NOTICE.md b/research/literal-positive-c-leaf/NOTICE.md new file mode 100644 index 0000000000..71c5f6dae2 --- /dev/null +++ b/research/literal-positive-c-leaf/NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and license + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +New material is Apache-2.0; copied predecessors retain their original notices. + +Jose Manuel (jmbarrancoml), CrocSwap/integer-mult-bounds#3091, supplies the +Gaussian C numerator rows, exact carry/parity/signed-fit argument, physical +complete-axis strategy and direct tensor tariff. Credit its #3055/#3087 +physical lineage, Alejandro Zarzuelo Urdiales's #45 Gaussian tensor reserve +and norm results, James Chang's #1869 ripple arithmetic, AAAmirinu's #2327 +prefix audit, and Nick Petalas's #2772/#3089 prefix/capacity work. + +@CubeJerry's #6967 current-coded leaf supplies the earlier source/format/ +lifecycle binding and explicitly leaves literal numerical export open. +#6978, #6986 and #6989 provide distinct all-source, cutoff-transport and +rounded wrappers. Their stronger failure-retirement and old coded interfaces +are not silently inherited by this packed component. + +The actual #7000 source, Clifford compiler and retained independent Gaussian +verifier are credited to DreamingOfClouds, Ali Romman, Cinna Davis, zxv, +unpaidmoon, icekylinx, CubeJerry and the earlier authors named by the retained +sources. The construction, lowering and matrix identities are not claimed anew. + +The packed ABI is published at +`172f4535ce8dcff79f626410af845f757c1563be`. Unary/Gamma/trace patterns follow +literal-layer-phase at `8b549ca6557ccbb3017b104b27ea35051f990416`, which credits +literal-layer-egress at `51ab0539059214fcfa044938c36a0b6017232be5`. The exact +Builder/Machine originates in #7349, head +`9dfe6747b8553fd11b408f2b045c5954ef1e6eaa`. + +The parent's dense execution/oracle and literal_layer_boundary's independent +source/Gaussian/universal-cost review are separately attributed in REVIEW.md. +Their artifacts are unchanged. Independent AI work is not human approval or +formal proof-kernel acceptance. diff --git a/research/literal-positive-c-leaf/OVERLAP.md b/research/literal-positive-c-leaf/OVERLAP.md new file mode 100644 index 0000000000..a32d3365cc --- /dev/null +++ b/research/literal-positive-c-leaf/OVERLAP.md @@ -0,0 +1,57 @@ +# Bounded source, novelty and complete-cost gate + +Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`. +Wave 4, tracks 20/85. The parent refreshed canonical state and active claims; +this worker performed targeted source/PR checks, not a full archive rescan. + +The exact claim is one fixed literal positive rank-one C tensor leaf on the +complete supplied packed field, including f>1, encoded cutoff, generated +axis geometry, original-owner commit and retained private histories. + +## Predecessors checked + +| Source | Actual established scope | Outstanding seam addressed here | +| --- | --- | --- | +| #3091 `physical-gaussian-leaf` | C/inverse scalar carry proof, exact prefix guards, complete physical axes, O(fV) structured source | A fixed local instruction graph at an encoded packed entry | +| #6967, head `61edc4fe348f0aeadc82a3b642a802cbfb03aed8` | Actual old current-coded/23-field rank-one leaf, 349 ports, stronger named-failure cleanup | Its proof explicitly leaves literal numerical export open | +| #6978 | All-source rank metadata transport around that numerical provider | Metadata literalization is not a literal numerical leaf | +| #6986 | Private f/cutoff rank transport for the old provider | Does not lower its C payload; the present rank-one guard does not replace global cutoff production | +| #6989 | Literal dynamic lift/round codecs around the unchanged exact positive leaf | Central exact C service remains the inherited structured source | +| #6974 | Protected old-source MOVE composition with numerical-provider premises | Different source/format lifecycle composition, not this fixed graph | +| Published literal-native-quadratic-phase | Five-Gamma packed common-grid diagonal phase | Supplies the compatible raw ABI; does not perform C mixing | + +Live metadata and body search used `Gaussian literal leaf`, followed by exact +canonical reads of both leaf proofs and the later wrapper claims. The actual +selected #7000 word, compiler and independent Gaussian verifier were reused +from shared authenticated source data, not cloned repeatedly. SOURCE-GATE.json +records exact MOVE24472, rank one, the two positive C columns and complete +source-recipe equality. No algebraic C identity or tensor reserve is new here. + +## Full budget and source format + +The gate required `O(fV+E)` at the new packed boundary, including actual +parameter decoding, helpers, source returns, every full-axis split/merge, +whole-field banks, numerical work, normal retirement and original-owner +commit. Unary guides are bounded by the real field volume; cutoff stays +binary because its represented value need not be so bounded. Explicit +per-role caps retain historical backing after erasure and on shrinkage. + +The old current-coded ABI is LSB oriented with three physical bits per +virtual symbol and a different 23-value header. The new MSB packed entry is +not silently substituted for it. The caller must provide the exact semantic +format/packing/header bridge with a complete bill. The source operator join +is exact; the entire old physical provider interface is not newly exported. + +The direct-leaf domain remains f<=cutoff, checked on encoded words. Rank one +still requires f C axes. Actual m=9,f=2 full-field execution and a first-axis- +only mutant check that distinction. Nonleaf replacement and global producer +admission are not inferred from this local bill. + +## Decision and limits + +The bounded searches found no matching complete literal C tensor leaf on +this boundary. The exact normalization gate and full budget passed. Scope +was kept separate from the concurrent selected SCALE wrapper and translation +descriptor work. The supplied old-format bridge, incomplete failure cleanup, +whole-source composition and all five global assumptions remain explicit. +A repository-wide novelty claim or exhaustion of unpublished work is not made. diff --git a/research/literal-positive-c-leaf/PR-DESCRIPTION.md b/research/literal-positive-c-leaf/PR-DESCRIPTION.md new file mode 100644 index 0000000000..d9d18816cb --- /dev/null +++ b/research/literal-positive-c-leaf/PR-DESCRIPTION.md @@ -0,0 +1,107 @@ +## Result and motivation + +The physical positive Gaussian leaf already has exact arithmetic and a direct +O(fV) source proof, but its literal numerical-table export remains open. +This package implements one fixed 6,826-location, 29-tape graph for the +positive rank-one central factor of the actual selected #7000 MOVE24472, +`["MOVE",415,3,99,false]`. + +Its exact kernel is `C=[[1+i,1-i],[1-i,1+i]]/2`, applied as `C^(tensor f)` +over all f columns. Rank one does not set f=1. The source binder recomputes +the actual lowering, both positive C columns and the complete local recipe, +including normalization and phase. + +## Exact scope and full cost + +The explicitly supplied packed field is `[P]x[2^f]^9x[S]`, with r Gaussian +coefficients per address on a common grid and w signed MSB bits per component. +Its six Gamma parameters are `f,r,P,S,w,cutoff`; the first five agree with the +published literal native phase ABI. The graph checks w>=2, f<=cutoff, every +Gaussian half, signed output range and exact complete cardinality. + +All variable axis strides are generated on tapes. Full suffix splitting, +four-row finite-carry arithmetic, MSB restoration and full-array merging +execute for every f axis. A protected private field remains separate from +public DATA until all axes succeed. Successful commit uses the original owner +and returns every head, private body/guard and opaque exterior. + +For `V=2PSr2^(9f)w` and header length E, the complete bill is +`T<=65536(fV+E+1)`, with private historical backing +`K_entry+64(V+E+1)`. Every helper, source return, copy, staging pass, install +and retirement is charged. Cutoff stays binary, so an arbitrarily large +threshold costs its encoded length. Shrinking clean calls do not rescan old +blank tails; histories are retained per actual owner/origin. + +The accepting domain requires integral signed outputs at every executed +axis. Final-image fit alone is insufficient: `[1,0,0,1]` maps finally to +`[0,1,1,0]` under the two-axis tensor but fails the first exact half. Public +DATA is preserved on these named rejections. Private failure cleanup/retry +is not claimed and is weaker than the structured #6967 lifecycle. + +## Novelty and predecessor credit + +#3091 supplies the Gaussian rows, carry/parity/range proof, tensor reserve, +physical axis strategy and direct tariff; none is claimed new. #6967 binds +that structured kernel to the old coded interface. #6978/#6986/#6989 add +different source, cutoff and rounding wrappers while retaining the literal +numerical seam. This contribution supplies a fixed local graph and complete +ownership/history proof at the named packed boundary. + +The packed ABI is credited to +[literal native quadratic phase](https://github.com/CubeJerry/integer-mult-bounds/tree/172f4535ce8dcff79f626410af845f757c1563be/research/literal-native-quadratic-phase). +Header/return patterns follow +[literal layer phase](https://github.com/CubeJerry/integer-mult-bounds/tree/8b549ca6557ccbb3017b104b27ea35051f990416/research/literal-layer-phase) +and its egress/#7349 lineage. All copied files have exact repository, +commit:path, blob and byte hashes in SOURCES.json. Frozen predecessors are +unchanged. No upstream PR number is invented for these review branches. + +## Reproduction and verification + +Tested base: `e54523517d0f03e58352e647c403a5af3e525a57`. + +```sh +cd research/literal-positive-c-leaf +python -I -W error -B bind_source.py +python -I -W error -B check.py +python -I -W error -B check_big.py +``` + +Optimized-Python runs use `-O` and reproduce the same structured receipts. +The last command requires a C++17 compiler named `c++`; it compiles the +included dense local-table interpreter in a temporary folder. No external +library or network download is needed. + +The author checks execute seven complete m=9,f=1 successes, six rejection +controls, a 2049-bit cutoff and three same-owner grow/shrink/regrow calls. +The actual unchanged m=9,f=2 graph executes all 262,144 addresses and +2,621,440 bits in 704,382,528 counted transitions, matching a direct tensor +polynomial oracle with all normal-retirement checks. A first-axis-only mutant +still retires correctly but fails that oracle; the endpoint-only witness +rejects without DATA writes. The local cutoff2 fixture is not a certified +global selected-producer packet. + +Separate root execution and mutation checks, including smaller fixed-dimension +fixtures, are explicitly distinguished from that author's full actual f=2 +trace. A separate peer independently authenticates sources, proves the +Gaussian spectral/geometry interface, checks 17,528 scalar components and +27 isolated axis cost cases, and derives exact scalar and whole-axis costs. +Unchanged reviews, portable commands and exact receipts are in independent/, +REVIEW.md and VERIFY.json. AI-assisted cross-review is not human or kernel +verification. + +## Limitations and kappa status + +**No new kappa; the complete multiplication bound remains conditional and +all five global assumptions remain.** This is a concrete direct-leaf +lowering, not an accelerated nonleaf or complete source caller. + +The old 23-value/three-bit-coded LSB interface and strided native placements +require an explicitly supplied, paid format/packing/header bridge. The two +surrounding monomials, full MOVE/compiler composition, failure retirement, +global cutoff/stock/precision admission and analytic recovery remain open. +Matching the local source operator does not discharge those obligations. + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance. +Credit Jose Manuel, Alejandro Zarzuelo Urdiales, Nick Petalas, James Chang, +AAAmirinu, the selected native/compiler authors and all retained predecessors +in NOTICE.md. New material is Apache-2.0. diff --git a/research/literal-positive-c-leaf/PR-TITLE.txt b/research/literal-positive-c-leaf/PR-TITLE.txt new file mode 100644 index 0000000000..cd382ff31f --- /dev/null +++ b/research/literal-positive-c-leaf/PR-TITLE.txt @@ -0,0 +1 @@ +Implement the positive rank-one native C tensor leaf with complete literal control and retained workspace accounting diff --git a/research/literal-positive-c-leaf/PROOF.md b/research/literal-positive-c-leaf/PROOF.md new file mode 100644 index 0000000000..a8ae6684d5 --- /dev/null +++ b/research/literal-positive-c-leaf/PROOF.md @@ -0,0 +1,297 @@ +# A literal positive C tensor leaf on the packed selected native field + +## 1. Source-bound scope and exact ABI + +At canonical `e54523517d0f03e58352e647c403a5af3e525a57`, the selected #7000 +native word has zero-based event 24472 `["MOVE",415,3,99,false]`. +Recomputing its actual before/after Clifford frames and source lowering gives +rank one. The retained independent Gaussian interpreter confirms that the +positive central factor has columns `((1+i)/2,(1-i)/2)` and +`((1-i)/2,(1+i)/2)`. Thus it is exactly + +`C = (1/2) [[1+i,1-i],[1-i,1+i]]`. + +This is the same C as Jose Manuel's #3091 and the current coded leaf #6967. +It is not an unnormalized Walsh butterfly. Entrance/exit monomials are still +separate; this package does not execute the complete MOVE. Source pins and +credit are in SOURCES.json and NOTICE.md. Rank one is one selected coordinate +per column: for positive column width f the central operator is +`C^(tensor f)`, not a single C. Every f factor is implemented, low bit first. + +The supplied packed ABI is the first-five-field interface of the literal +native phase package at CubeJerry commit +`172f4535ce8dcff79f626410af845f757c1563be`, extended by one cutoff field. +HEADER contains six positive canonical Gamma codes, in order: + +`f, r, P, S, w, cutoff`. + +Here r is coefficient multiplicity, not source Fourier rank. Let E be the +total length of these codes. DATA is the complete lexicographic array +`[P] x [2^f]^9 x [S]`, with r Gaussian coefficients per address. Each has +w signed two's-complement real bits followed by w signed imaginary bits, +MSB first. All coefficients share an arbitrary fixed common grid, unchanged +by this program. Write `N=P S r 2^(9f)` and `V=2Nw`. + +Require `w>=2` and `f<=cutoff`; both are physically checked. DATA is exactly +V bits followed by a blank. HEADER may have opaque symbols after the sixth +code. Both public heads start at their origins. Supply 27 genuinely distinct +private tape owners, blank from one cell before each origin through the caps +in Section 6. Opaque exteriors are preserved on successful legal calls. +Origins may differ or be negative; the controller never decodes them. + +This is an explicit packed boundary, not the full old #6967 ABI. That provider +uses a 23-value length/unary-prefix/LSB descriptor and three-bit coded LSB +component fields with delimiters. A caller must supply the exact semantic +packing, component orientation, delimiter and header bridge, with its full +cost and ownership contract. Reversing individual already packed components +is linear, but the old codec and arbitrary strided packing are not silently +implemented here. The first five new fields match the published phase ABI; +its opaque-tail contract permits preservation of the added cutoff code. + +## 2. Universal accepting and failure contract + +For every legal encoded entry, suppose each output component of every +executed C axis is integral on the common grid and lies in +`[-2^(w-1),2^(w-1)-1]`. Then the fixed graph replaces DATA by the exact positive +`C^(tensor f)` on all f bits of coordinate zero. All eight other coordinates, +prefixes, suffixes, coefficient indices and absolute phase are preserved. +HEADER, every head, private body/guard and opaque exterior is restored; +DATA remains its original owner. + +At each executed scalar row the program rejects exactly a nonintegral half +or an out-of-range w-bit result. A finite missing or extra DATA bit is detected +by the header-derived clone before numerical execution. Width/cutoff failures +reject before the clone. These rejections precede every DATA write, so the +original public field/header remain intact. Missing local branches are +explicit reject endpoints in the reference interpreter. Failure-time private +retirement, head return and same-bank retry are not claimed. This is a weaker +failure lifecycle than structured #6967, not its full drop-in export. + +The domain is a prefix condition: final tensor-image fit alone does not +establish it. A credited sufficient condition from #3091 and its Gaussian +reserve/norm predecessors is that input components are divisible by +`2^ceil(f/2)`, bounded by M, and `2^ceil(f/2) M <= 2^(w-1)-1`. +This supplies all integral signed prefixes. Those reserve/norm results are +inherited, not new claims here. A caller can instead prove its actual +correlated prefix conditions. + +For a concrete obstruction to endpoint-only admission, the real f=2 fibre +`[1,0,0,1]` has final `C tensor C` image `[0,1,1,0]`. Its first low-bit-axis +pair `(1,0)` nevertheless produces nonintegral halves. The exact program +must reject it even though the final image is integral and fits at w=2. + +## 3. Literal acquisition and generated geometry + +`compile_leaf()` has no runtime arguments. Its 6,826-location graph uses 29 +fixed tapes and `{blank,0,1,|}`, with only scanned-symbol branches, one-cell +writes, unit moves, fixed jumps and halt. Compile-time loops enumerate fixed +bit/carry possibilities, never input-sized code. Varying counts and geometry +stay on tapes. + +The first five Gamma codes become unary guides by repeated `v -> 2v+b` +copies. Strict binary prefixes sum to less than the represented value, so +these conversions cost `O(f+r+P+S+w+E)=O(V+E)`. The first value's canonical +binary word and bit length are also copied. Cutoff is copied only in binary, +with a unary bit length. Comparing lengths and, only if equal, MSB words +checks `f<=cutoff`. An arbitrarily large represented cutoff thus costs O(E), +not its value. HTRACE records every public header advance and restores its +head without an origin oracle. All comparison words are retired afterwards. + +For axis j, `0<=j=2: the initial width-guided seek, w digit transitions, +two sign extensions, parity/range scans, output emission and all returns are +included. Each ordinary digit uses at most thirteen instructions. The four +input loads plus clears cost at most `84w+44`. Four scalar rows, pair control +and component handling therefore cost at most 640w per pair. There are +N/2 pairs per complete axis. All half loads, stream merges, whole-field +returns, suffix/prefix loops and their resets are linear scans of V; their +loops have fixed depth and every range is nonempty. A conservative count +places a complete axis, including its geometry update when present, below +`8192(V+1)` instructions. The actual table has no per-bit scan of a full +descriptor or whole address word. + +Separately, header/initial geometry/source clone and final commit/retirement +are each below `8192(V+E+1)`: the preceding exact unary-helper prices and +constant-many full scans give much smaller coefficients, and this allowance +also covers all fixed guard and branch instructions. Hence + +`T <=8192[f(V+1)+2(V+E+1)] <=65536(fV+E+1)`. + +The second inequality uses f,V>=1. This is a complete direct-leaf bill: +source access and return, geometry, every axis, copying, full staging, +installation and erasure are charged. It is not a faster nonleaf tariff. +The fixed program construction is input independent. Entry acquisition, +old-format conversion, source packing and transport to the entry heads are +supplied caller work and must be added where required. + +For backing, put `U*=Sr 2^(9f-1)`, `A*=P 2^(f-1)`, and +`C*=max(A*,U*,f,r,P,S,w)`. Relative to its own origin, each private role visits +only `[-1,cap]`, including the guard and blank endpoint, with these caps: + +| Role | cap | +| --- | --- | +| A, B, DTRACE | V on each role | +| MODE | 1 | +| HTRACE, LENGTH | E on each role | +| DOUBLE | C* | +| F, R, P, S, WIDTH | f,r,P,S,w respectively | +| FBIN, FLEN | ell(f) on each role | +| TBIN, TLEN | ell(cutoff) on each role | +| PREFIX, SUFFIX | A*, U* respectively | +| LEFT, RIGHT, LOUT, ROUT | `2w U*` on each role, using the maximum U* | +| AR, AI, BR, BI | w on each role | +| NUM | w+2 | + +Every cap in the twenty volume-type roles is <=V, except NUM's harmless +additional two cells; six code-type roles are <=E, and MODE needs one cell. +Including 27 guards/endpoints, their total allowance is at most +`20V+6E+57 <=64(V+E+1)`. Here K0 counts the actual pre-entry historical +backing of the 27 private owners only. Their backing at every time is at most + +`K0+64(V+E+1)`. + +For a complete 29-owner history statement, include all public history in K0 +and add at most `E+V+2` public head positions. The same loose envelope remains +valid, since `21V+7E+59 <=64(V+E+1)`. Supplied source/opaque entry backing is +included in actual K0; a test fixture's unpriced construction is not a theorem +about free caller acquisition. + +Erasure never subtracts historical cells. All successful-call writes are +blank again at return; older tails are already blank from prior successes. +Thus a smaller clean call needs no scan of old capacity and retains its own +current-shape time bound. At fixed origins repeated calls use per-role maxima, +then sum. Under changing origins retain absolute per-role history unions and +the caller's paid transport corridors; do not replace them by maximum current +volume. Whole-tail blankness and genuinely distinct owned windows are entry +premises, not inferred from a few local reads or fresh wrapper identities. + +## 7. Exact source transfer, evidence and unresolved interfaces + +The selected native tensor convention packs coordinate i as +`a_i=sum_j x_(j,i) 2^j`. The central rank-one compiler factor acts on i=0 in +each column j. The identity of its two source columns, with denominator two, +therefore identifies the operator implemented above exactly, including phase +and normalization. The source binder checks the entire retained local recipe; +this does not claim that this package implements its two surrounding factors. + +For a current coded caller, an admitted semantic bridge must identify these +actual bits, preserve the complete other coordinate/spectator/coefficient +fields, preserve the common grid and signed width, and supply the six values +above, including the actual cutoff. It must price real packing and coefficient +orientation. The generic #6967 domain contains shapes that are not already +this complete packed nine-coordinate tensor; those calls are not silently +included. A supplied view cannot make strided payload movement free. + +The author checker uses a direct tensor-row Gaussian polynomial oracle, +not the executable butterfly/carry algorithm. It tests complete m=9,f=1 +packets, endpoint values, coefficient/spectator multiplicities, both named +arithmetic failures, cardinality/width/cutoff failures and a 2049-bit threshold. +The separate C++ interpreter executes the same fixed 6,826-location table on +the complete actual m=9,f=2 array: 262,144 addresses, 2,621,440 bits, and +704,382,528 table instructions. Its output matches the independent direct +tensor formula, and every header/head/private/exterior check passes. It +cross-checks the original interpreter at f=1. A mutant that executes only +the first axis still retires correctly but fails the f=2 tensor oracle, +directly detecting rank-one/f=1 conflation. No reduced dimension substitutes +for that actual full-field f=2 execution. + +Independent root/peer evidence is recorded separately in REVIEW.md. Finite +tests support, but do not replace, the universal graph invariants and cost +proof above. Open obligations remain: full old-codec and placement bridges, +failure retirement if required, entire source MOVE/caller composition, +global producer/cutoff/precision admission, nonleaf speed and the other +foundational assumptions. No selected certificate, new kappa or unconditional +integer-multiplication theorem is claimed. diff --git a/research/literal-positive-c-leaf/README.md b/research/literal-positive-c-leaf/README.md new file mode 100644 index 0000000000..b86c07d7fa --- /dev/null +++ b/research/literal-positive-c-leaf/README.md @@ -0,0 +1,102 @@ +# A positive native C tensor leaf as one literal tape program + +**Scoped numerical/interface lemma. No new kappa; all five selected global +assumptions remain.** Prepared for Jerry Chen / @CubeJerry with substantial +OpenAI assistance. + +One fixed 6,826-location, 29-tape graph executes the positive rank-one central +child of actual #7000 MOVE24472, `["MOVE",415,3,99,false]`. The scalar factor +is `C=[[1+i,1-i],[1-i,1+i]]/2`; for column width f it executes the entire +`C^(tensor f)`. Rank one does not mean f=1. + +The supplied entry is the packed `[P]x[2^f]^9x[S]` field of the published +literal native phase component, with r common-grid Gaussian coefficients +per address, w signed MSB bits per component, and six Gamma values +`f,r,P,S,w,cutoff`. Its first five fields agree with that phase ABI; its +opaque-tail contract preserves the added cutoff. The old 23-field coded +descriptor conversion and strided packing remain supplied caller work. + +## Result and complete bill + +The program generates all f axis strides, splits complete suffix blocks, +executes exact four-input Gaussian rows, checks parity and final signed fit, +restores MSB order and merges full arrays. Two persistent private field banks +alternate. DATA commits on its original owner only after every axis succeeds. + +For `N=PSr2^(9f)`, `V=2Nw` and header length E: + +`T<=65536(fV+E+1)`, private history `<=K_entry+64(V+E+1)`. + +Metadata, source access/return, every axis, full staging, installation, resets +and erasure are included. Cutoff stays binary, so a huge threshold costs its +encoded length. All heads/private bodies/guards return on success. Erased +history remains charged, and smaller clean calls scan only current shapes. + +The accepted numerical domain requires integral w-bit outputs at every axis. +Final-image fit is insufficient: real f=2 fibre `[1,0,0,1]` has final image +`[0,1,1,0]`, but its first axis is half-integral and must reject. Named arithmetic +and finite width/cutoff/cardinality failures preserve public DATA. Failure +private cleanup/retry is not claimed, unlike the stronger structured #6967 +lifecycle. + +## Contribution and predecessor boundary + +#3091 already supplies the C identities, tensor reserve, physical axis method +and direct O(fV) tariff. #6967 binds its structured implementation to the old +current-coded interface; subsequent rounded/cutoff wrappers leave literal +numerical lowering open. This package adds a fixed local-symbol graph, +generated geometry, same-owner staging and retained-history proof at the +explicit packed boundary. The exact source gate recomputes MOVE24472 and its +positive normalization. Its two surrounding monomials, full old codec, +complete MOVE, enclosing compiler and nonleaf speed remain outside the claim. + +## Reproduce + +With Python 3.10+ from this directory: + +```sh +python -I -W error -B bind_source.py +python -I -W error -B check.py +python -I -W error -B check_big.py +``` + +Add `-O` for optimized Python. `check_big.py` also requires a C++17 compiler +named `c++`; it compiles the included table interpreter in a temporary folder. +No downloaded library is needed. C++ interprets the same literal table; it is +test infrastructure, not an additional machine-model operation. + +Eleven exact source/blob pins and wrong-rank/inverse-C controls protect the +source gate. Seven complete m=9,f=1 Python successes use 6,201,327 transitions; +six malformed/arithmetic packets preserve DATA. Three grow/shrink/regrow calls +retain the same 29 owners and private history 42,093. + +The complete **actual m=9,f=2** execution has 262,144 addresses, 2,621,440 bits +and 704,382,528 literal transitions. A direct tensor-row polynomial oracle +agrees, with every header/head/private/exterior check passing. A first-axis-only +mutant retires correctly but fails that oracle. The complete endpoint-only +fibre above rejects with zero DATA writes. The C++ interpreter also matches +the original interpreter's exact f=1 count. This local f=2 packet uses cutoff +2; it is not a globally certified selected-producer witness. + +[PROOF.md](PROOF.md), [RESULT.json](RESULT.json), [BIG-RESULT.json](BIG-RESULT.json) +and [SOURCE-GATE.json](SOURCE-GATE.json) contain claims and receipts. +[REVIEW.md](REVIEW.md) separates root execution, smaller-dimension fixtures, +the author's actual full f=2 trace and peer universal/source review. These +are AI-assisted checks, not human or proof-kernel acceptance. +[VERIFY.json](VERIFY.json) and [VALIDATION.md](VALIDATION.md) provide replay +commands and executed gates; [SOURCES.json](SOURCES.json) fixes all inputs. + +## Open next questions + +1. **Whole selected MOVE.** Join the literal right monomial, central tensor + and left monomial in exact order on a protected shadow owner. Separate + kernels alone do not make their composition publicly failure-atomic. +2. **Actual source bridge.** Lower the old codec, placement and descriptor + translation, charging all payload movement and returns. Start from one + exact producer; generic strided packing is not cheap header preparation. +3. **Failure retirement.** Construct a priced cleanup continuation if callers + require private-bank retry after a bad prefix. Present failure protection + covers public DATA only. +4. **Global theorem.** Bind producer, cutoff, precision and stock costs to the + full recurrence while retaining a faster nonleaf service. This local direct + leaf does not resolve those dependencies or improve kappa. diff --git a/research/literal-positive-c-leaf/RESULT.json b/research/literal-positive-c-leaf/RESULT.json new file mode 100644 index 0000000000..acdb46646f --- /dev/null +++ b/research/literal-positive-c-leaf/RESULT.json @@ -0,0 +1,113 @@ +{ + "locations": 6826, + "rejected_steps": 908755, + "rejections": 6, + "repeated_history": { + "calls": 3, + "owner_inventory": 29, + "private_history": [ + 42093, + 42093, + 42093 + ], + "steps": [ + 1305638, + 376628, + 1305638 + ] + }, + "scope": "Complete physical f=1 packets; f>1 covered separately, not inferred from rank1.", + "seed": 2026111204, + "source_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", + "sources": 11, + "status": "PASS_LITERAL_C_AUTHOR_BASE", + "successes": [ + { + "kind": "constant signed endpoint", + "shape": [ + 1, + 1, + 1, + 1, + 2, + 1 + ], + "steps": 376628 + }, + { + "kind": "constant signed endpoint", + "shape": [ + 1, + 1, + 1, + 1, + 3, + 1 + ], + "steps": 514892 + }, + { + "kind": "constant signed endpoint", + "shape": [ + 1, + 1, + 1, + 1, + 3, + 1 + ], + "steps": 514892 + }, + { + "kind": "dirty complete spectators and coefficients", + "shape": [ + 1, + 2, + 1, + 1, + 4, + 1 + ], + "steps": 1305608 + }, + { + "kind": "dirty complete spectators and coefficients", + "shape": [ + 1, + 1, + 2, + 1, + 5, + 3 + ], + "steps": 1568434 + }, + { + "kind": "dirty complete spectators and coefficients", + "shape": [ + 1, + 1, + 1, + 2, + 4, + 2 + ], + "steps": 1305648 + }, + { + "kind": "binary cutoff", + "shape": [ + 1, + 1, + 1, + 1, + 3, + "2049-bit threshold" + ], + "steps": 615225 + } + ], + "successful_steps": 6201327, + "table_sha256": "ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9", + "tapes": 29 +} diff --git a/research/literal-positive-c-leaf/REVIEW.md b/research/literal-positive-c-leaf/REVIEW.md new file mode 100644 index 0000000000..ad77c71266 --- /dev/null +++ b/research/literal-positive-c-leaf/REVIEW.md @@ -0,0 +1,72 @@ +# Independent review and scopes of execution evidence + +**Disposition: accepted for the stated packed positive direct-leaf theorem.** +The separate peer accepts the universal source/numerical/cost/history proof; +the parent's separately implemented dense execution and mutation checks pass. +These are independent AI-assisted checks, not human or proof-kernel acceptance. + +## Exact frozen science + +- `leaf.py`: SHA256 `bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744`. +- `PROOF.md`: SHA256 `c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c`. +- Graph plus alphabet canonical JSON: SHA256 `ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9`. + +No program modification was requested by either reviewer. The final proof +clarifies that suffix-bank caps use maximum U* and distinguishes the private +K0 statement from the optional all-owner history statement. + +## Root independent CPU and tensor oracle + +`independent/dense_check.py` and its two receipts are unchanged copies of the +parent's separately written interpreter and tensor-polynomial oracle. The +normal and optimized receipts agree. It reports seven actual m=9 cases, +267 explicitly smaller fixed-dimension fixtures, 111 successes and 167 +rejections including controls, and 9,782,553 successful transitions. It tests +all 256 width-two Gaussian pairs in the smaller fixtures, a 2049-bit cutoff, +header/owner/head/exterior/private restoration and persistent-history reuse. + +Four actual graph mutants are detected: conjugate instead of positive C, +admitting odd numerator halves, truncating signed overflow, and corrupting +original-owner installation. The receipt explicitly says that this root +suite has **no complete actual m=9,f=2 success**. Its smaller fixtures are +not relabelled as such a run. + +```sh +python -I -W error -B independent/dense_check.py leaf.py +``` + +## Separate source, spectral and universal-cost review + +The `literal_layer_boundary` agent's unchanged review, checker and both +receipts are in `independent/peer/`. It independently checks all eleven exact +source bindings, the selected normalization, Walsh-spectral C tensor kernels +through eight axes, geometry, signed-prefix admission and retained backing. +It also executes 17,528 isolated component cases with 8,132 acceptances, +checks 27 isolated guide-driven axes, and derives exact costs +`43w+57` per successful component and `99V+153N+48A+16` per completed axis +before next-axis geometry or final commit. Those are local cost slices, +not complete selected packets. Three component graph mutants are detected. + +```sh +python -I -W error -B independent/peer/check.py . +``` + +## Author's actual full f=2 trace + +The author separately wrote `table_cpu.cpp`, a dense interpreter of the same +fixed table, and `check_big.py`, which compares its complete output against +the direct tensor-row polynomial oracle. The actual m=9,f=2 run is all +262,144 addresses, 2,621,440 bits and 704,382,528 counted instructions. +All normal retirement checks pass; its exact output hash is in BIG-RESULT.json. +The C++ interpreter's f=1 count agrees with the original reference interpreter. + +A first-axis-only mutant preserves owner, length and normal retirement but +fails the full f=2 oracle. A second complete f=2 fixture has a fitting integral +final tensor image but rejects its first nonintegral prefix with zero DATA +writes. Its dirty private state is recorded honestly; failure cleanup is not +claimed. This author evidence fills a runtime scope absent from the root's +suite, but it is not renamed independent peer or human verification. + +All finite evidence is distinguished from the universal proof and its +explicit supplied-format, common-grid, ownership and caller premises. No +global assumption, entire MOVE, nonleaf rate or new kappa is certified. diff --git a/research/literal-positive-c-leaf/SOURCE-GATE.json b/research/literal-positive-c-leaf/SOURCE-GATE.json new file mode 100644 index 0000000000..ef13582d6b --- /dev/null +++ b/research/literal-positive-c-leaf/SOURCE-GATE.json @@ -0,0 +1,125 @@ +{ + "canonical_native_sha256": "91429a6b96729292a8764836e00c87a6f7cd3b76f05159033f4867f69a98d097", + "event": [ + "MOVE", + 415, + 3, + 99, + false + ], + "event_index": 24472, + "factor": "C tensor f, not f=1", + "negative_controls": [ + "wrong central rank", + "conjugate/inverse C" + ], + "positive_C_columns": [ + [ + { + "0": [ + 1, + 1 + ], + "1": [ + 1, + -1 + ] + }, + 1 + ], + [ + { + "0": [ + 1, + -1 + ], + "1": [ + 1, + 1 + ] + }, + 1 + ] + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 3, + 5, + 9, + 17, + 32, + 65, + 129, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 3, + 3, + 3, + 3, + 0, + 3, + 3, + 2, + 0 + ], + "matrix_rows": [ + 239, + 129, + 130, + 132, + 136, + 16, + 160, + 192, + 256 + ], + "offset": 1, + "phase": 1, + "quadratic_rows": [ + 111, + 111, + 111, + 111, + 0, + 111, + 111, + 0, + 0 + ] + } + }, + "scope": "Source operator binding only; full MOVE and old-format/packing bridges remain supplied.", + "source_files": 11, + "status": "PASS_LITERAL_C_CURRENT_SOURCE" +} diff --git a/research/literal-positive-c-leaf/SOURCES.json b/research/literal-positive-c-leaf/SOURCES.json new file mode 100644 index 0000000000..fd408e3f26 --- /dev/null +++ b/research/literal-positive-c-leaf/SOURCES.json @@ -0,0 +1,104 @@ +{ + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "local": "reference/current-coded-README.md", + "path": "research/current-coded-gaussian-leaf/README.md", + "blob": "753a44f2b392d8a0297cb1324be396f246f69935", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bytes": 3618, + "sha256": "5554fdac912fcb92a7833a8b860f8d21962f78eb2a4087d3688f476b891db2f3" + }, + { + "local": "reference/current-coded-PROOF.md", + "path": "research/current-coded-gaussian-leaf/PROOF.md", + "blob": "3479c700c9b68968106454e57993e9615cc6a821", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bytes": 16938, + "sha256": "f01a2c81805eed7f6983d9928258100a00a7c8e6f2532bf10610c0883c7e972d" + }, + { + "local": "reference/physical-C-PROOF.md", + "path": "research/physical-gaussian-leaf/PROOF.md", + "blob": "e98db470cdb8bfc49e9da86c39c0d6ae16e92716", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bytes": 12417, + "sha256": "29ebd43146f921077f980a408915ecc3a5199a07fcdadc624a8282c06b0b8104" + }, + { + "local": "reference/clifford_exact.py", + "path": "research/shared-wire-split-composition/frozen/clifford_exact.py", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "bytes": 6824, + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "local": "reference/native_verify.py", + "path": "research/shared-wire-split-composition/frozen/native_verify.py", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "bytes": 12323, + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "local": "reference/selected-native.json.gz", + "path": "research/shared-wire-split-composition/data/final.json.gz", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "blob": "74563a7867d9d762b6588f65362369668841bb3e", + "bytes": 350722, + "sha256": "2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883" + }, + { + "local": "reference/selected-native-catalogue.py", + "path": "docs/research/pr-intake-evidence/pr7000-application/check_native_catalogue.py", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "blob": "98b35c89c8bd52637633aa78d506244bca8ec9e1", + "bytes": 5071, + "sha256": "6120e1ea1e07eeba757694d209437a38f121b0a377cc466889a30fa52c561472" + }, + { + "local": "reference/02-streams.tex", + "path": "upstream/build/sections/02-streams.tex", + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "blob": "088fceea1867abc76271d7efe7532b779fee9039", + "repository": "CrocSwap/integer-mult-bounds", + "bytes": 11311, + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "local": "inputs/controller_reference.py", + "path": "research/selected-rank-control/controller_reference.py", + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa", + "blob": "3ab6d0361f35038ffcdf0cf81a157f7a17b40e72", + "repository": "CubeJerry/integer-mult-bounds", + "bytes": 5938, + "sha256": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73" + }, + { + "local": "reference/phase-patterns.py", + "path": "research/literal-layer-phase/phase.py", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "8b549ca6557ccbb3017b104b27ea35051f990416", + "blob": "c6e87695340a12d76d8f4fc8fb9ae069d3ec6a47", + "bytes": 11572, + "sha256": "9a360817b80e869398927f38a4f110de0b5a1f9620eeb23b19e166f112b83f23" + }, + { + "local": "reference/packed-phase-PROOF.md", + "path": "research/literal-native-quadratic-phase/PROOF.md", + "repository": "CubeJerry/integer-mult-bounds", + "commit": "172f4535ce8dcff79f626410af845f757c1563be", + "blob": "46a43bf214d828aa972db66ad35e41b9cd07a964", + "bytes": 17878, + "sha256": "55f0a575f618bf467d0e25a25802053455d701cee1f23fb8811a671a1bd59ff3" + } + ] +} diff --git a/research/literal-positive-c-leaf/TASK.json b/research/literal-positive-c-leaf/TASK.json new file mode 100644 index 0000000000..c67f3125e7 --- /dev/null +++ b/research/literal-positive-c-leaf/TASK.json @@ -0,0 +1,45 @@ +{ + "task": "literal-positive-rank-one-C-leaf", + "wave": 4, + "tracks": [ + 20, + 85 + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "worker": "crt_reusable_history", + "branch": "research/literal-positive-c-leaf-be42-wave4", + "status": "verified complete; independent universal proof/source and dense runtime accepted", + "started_utc": "2026-11-12T03:37:44.883071+00:00", + "source_occurrence": { + "event": 24472, + "token": [ + "MOVE", + 415, + 3, + 99, + false + ], + "rank": 1, + "operator": "C1=(1/2)[[1+i,1-i],[1-i,1+i]], tensor-powered over all f columns" + }, + "exact_scope": "Fixed m=9 literal graph on packed [P]x[2^f]^9x[S] arrays, r Gaussian w-bit MSB components per address on one common grid; six positive Gamma fields f,r,P,S,w,cutoff, first five matching the prior literal native phase ABI. Execute all f C axes of coordinate zero, guard f<=cutoff and w>=2, exact halves and signed fit, stage entire call, original-owner commit and normal private retirement.", + "optimistic_budget": "V=2PSr*2^(9f)*w, header length E. O(fV+E) time and K_entry+O(V+E) private backing. Each axis uses generated prefix P*2^(f-1-j), suffix coefficient count Sr*2^(8f+j). Full per-axis splitting, exact four-input arithmetic, merging, private-bank retirement, source clone/return and final commit are paid. Cutoff stays binary so very large cutoff costs O(E), not its represented value.", + "abi_bridge": "Current #6967 is three-bit-coded LSB fields with a 23-value header. A source caller must supply the exact semantic format/packed-layout and header bridge; it is not silently implemented here. Rank1 means C tensor f, not f=1. The new packed first-five-field ABI matches the literal native phase package.", + "exclusions": [ + "No whole old23-field caller or free strided packing.", + "No accelerated nonleaf or global cutoff/precision theorem.", + "No new kappa or foundational-assumption discharge.", + "Arithmetic rejection preserves public DATA but private failure retirement is not claimed unless implemented and proved." + ], + "prior_work": [ + "#3091 scalar Gaussian identities, finite carry, tensor-grid reserves and physical direct tariff are credited.", + "#6967 source/current-format leaf and #6989 rounded wrapper retain literal numerical lowering open.", + "Distinct from A4 SCALE1125 wrapper binding." + ], + "stopping_rule": "Stop for matching existing literal tensor leaf, incompatible complete tariff, or source-normalization/format mismatch. One evidence-driven pivot allowed.", + "next_action": "Parent reviews final scoped local commit and publishes; scientific bytes frozen.", + "program_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", + "proof_sha256": "c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c", + "full_f2_receipt": "BIG-RESULT.json: actual fixed m9 graph, 262144 addresses, 704382528 instructions; separate C++ table interpreter plus direct tensor oracle", + "accepted_proof_sha256": "c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c" +} diff --git a/research/literal-positive-c-leaf/VALIDATION.md b/research/literal-positive-c-leaf/VALIDATION.md new file mode 100644 index 0000000000..57556d7afe --- /dev/null +++ b/research/literal-positive-c-leaf/VALIDATION.md @@ -0,0 +1,54 @@ +# Executed validation + +Completed on 2026-11-12T04:11:07.837895+00:00 with Python 3.12.14. +C++ compiler: c++ (Debian 14.2.0-19) 14.2.0; compiled with -std=c++17 -O2. + +All eight commands in VERIFY.json were executed successfully. The three author +normal/optimized structured output pairs are byte-identical. Both relocated +independent commands reproduce their saved structured receipts exactly. + +```sh +python -I -W error -B bind_source.py +python -I -W error -O -B bind_source.py +python -I -W error -B check.py +python -I -W error -O -B check.py +python -I -W error -B check_big.py +python -I -W error -O -B check_big.py +python -I -W error -B independent/dense_check.py leaf.py +python -I -W error -B independent/peer/check.py . +``` + +## Exact receipts + +- RESULT.json: SHA256 `ddae895317a1df60b94959694052b34a881763de4112f57a0efe4be01dd9bf1e`. +- SOURCE-GATE.json: SHA256 `66b0d2dcca39275434e2743b061aafe8b4968dec2440b6444c5058dc54f3b126`. +- BIG-RESULT.json: SHA256 `f499bde45dd018e991c480ebbc0d93a5d0a88495a438c7c099cf3dd5a1d4f3b8`. +- independent/DENSE-RESULT.json: SHA256 `fe3831e67a7db6ce9aca525d9ad02ff55e5751b9f12892d745b7afbb2782ae62`. +- independent/peer/RESULT.json: SHA256 `2c45ae6e55e35e5caabcabb21addae62fa1e9acf964f6128df71c1f107118826`. + +## Coverage and limits + +The author Python suite has seven complete m9 f1 successes (6,201,327 steps), +six rejections (908,755 steps), and three same-owner calls with retained private +history [42093,42093,42093]. Their step counts are [1305638,376628,1305638]. +The cutoff fixture has 2049 encoded bits. All eleven source pins match. + +The actual fixed m9 f2 table executes the entire 262,144-address, 2,621,440-bit +packet in 704,382,528 steps. Full output, public write counts, all heads, private +blankness, header and opaque exteriors match the direct tensor oracle. The +first-axis-only mutant executes 401,212,870 steps and is detected despite +normal retirement. The complete endpoint-only f2 fixture rejects in 36,898,051 +steps with zero DATA writes; dirty private state is intentionally recorded. + +The C++ interpreter checks its f1 count against the original interpreter. Its +run times in BIG-TIMING.txt are environment observations, not model costs or +complexity improvements. No reduced dimension replaces the author full f2 run. + +The root uses separate full m9 f1 and explicitly smaller fixed-dimension +fixtures; its receipt does not claim a complete actual m9 f2 success. The peer +uses separate source/spectral proofs and isolated component/axis cost slices. +All independent artifacts are unchanged and their scopes are preserved. + +No full MOVE, current old-codec/placement producer, nonleaf tariff, selected +cold replay, global-assumption discharge, human or proof-kernel acceptance +is claimed. See PROOF.md and REVIEW.md for the exact remaining obligations. diff --git a/research/literal-positive-c-leaf/VERIFY.json b/research/literal-positive-c-leaf/VERIFY.json new file mode 100644 index 0000000000..9296bc1e52 --- /dev/null +++ b/research/literal-positive-c-leaf/VERIFY.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "C++17 compiler available as c++ for check_big.py" + ], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/bind_source.py" + ], + "timeout_seconds": 60, + "checks": "Eleven exact sources, actual MOVE24472 rank/normalization and two source controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/bind_source.py" + ], + "timeout_seconds": 60, + "checks": "Eleven exact sources, actual MOVE24472 rank/normalization and two source controls under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/check.py" + ], + "timeout_seconds": 180, + "checks": "Actual m9 f1 packets, signed/cutoff/cardinality controls and persistent-history reuse" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/check.py" + ], + "timeout_seconds": 180, + "checks": "Actual m9 f1 packets, signed/cutoff/cardinality controls and persistent-history reuse under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/check_big.py" + ], + "timeout_seconds": 180, + "checks": "Actual unchanged m9 f2 complete field with separate C++ table interpreter, direct tensor oracle and two all-column/endpoint controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/check_big.py" + ], + "timeout_seconds": 180, + "checks": "Actual unchanged m9 f2 complete field with separate C++ table interpreter, direct tensor oracle and two all-column/endpoint controls under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent/dense_check.py", + "{package}/leaf.py" + ], + "timeout_seconds": 180, + "checks": "Root separate CPU/direct tensor polynomial oracle; actual m9 f1 and explicitly smaller fixed-dimension fixtures; four executable mutations" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent/peer/check.py", + "{package}" + ], + "timeout_seconds": 180, + "checks": "Separate source/spectral/universal-cost review; exact scalar/axis graph cost and negative controls" + } + ] +} diff --git a/research/literal-positive-c-leaf/bind_source.py b/research/literal-positive-c-leaf/bind_source.py new file mode 100644 index 0000000000..3b6db7deca --- /dev/null +++ b/research/literal-positive-c-leaf/bind_source.py @@ -0,0 +1,63 @@ +"""Replay the exact current selected source/rank/positive-C normalization gate.""" +from pathlib import Path +import copy +import gzip +import hashlib +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from check import authenticate, require + + +def module(name,path): + spec=importlib.util.spec_from_file_location(name,path) + result=importlib.util.module_from_spec(spec) + sys.modules[name]=result + spec.loader.exec_module(result) + return result + + +def main(): + source_count=authenticate() + C=module('literal_c_compiler',HERE/'reference/clifford_exact.py') + V=module('literal_c_independent',HERE/'reference/native_verify.py') + raw=(HERE/'reference/selected-native.json.gz').read_bytes() + require(hashlib.sha256(raw).hexdigest()=='2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883', + 'selected source compressed pin') + word=json.loads(gzip.decompress(raw)) + canonical=hashlib.sha256(json.dumps(word,sort_keys=True,separators=(',',':')).encode()).hexdigest() + require(canonical=='91429a6b96729292a8764836e00c87a6f7cd3b76f05159033f4867f69a98d097', + 'selected source semantic pin') + event=word['program'][24472] + require(event==['MOVE',415,3,99,False], 'actual selected occurrence') + a=C.canonical_frame(9,tuple(word['frames'][3])) + b=C.canonical_frame(9,tuple(word['frames'][99])) + recipe,_=C.lower_child(a.adjoint().then(b)) + require(recipe['rank']==1, 'rank-one child') + target=V.adjoint(V.frame(word['frames'][3],9))+V.frame(word['frames'][99],9) + V.equal(V.recipe(recipe),target,'actual selected complete recipe') + columns=[V.state(V.fourier(1),basis) for basis in (0,1)] + require(columns==[({0:(1,1),1:(1,-1)},1),({0:(1,-1),1:(1,1)},1)], + 'positive C absolute normalization') + wrong=copy.deepcopy(recipe);wrong['rank']=2 + try: + V.equal(V.recipe(wrong),target,'wrong central rank') + except ValueError: + pass + else: + raise ValueError('rank mutant survived') + require([V.state(V.adjoint(V.fourier(1)),b) for b in (0,1)]!=columns, + 'inverse C mistaken for positive C') + print(json.dumps({'status':'PASS_LITERAL_C_CURRENT_SOURCE','event_index':24472, + 'event':event,'rank':1,'factor':'C tensor f, not f=1','source_files':source_count, + 'positive_C_columns':columns,'canonical_native_sha256':canonical, + 'recipe':recipe,'negative_controls':['wrong central rank','conjugate/inverse C'], + 'scope':'Source operator binding only; full MOVE and old-format/packing bridges remain supplied.'}, + indent=2,sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/literal-positive-c-leaf/check.py b/research/literal-positive-c-leaf/check.py new file mode 100644 index 0000000000..ca871e9665 --- /dev/null +++ b/research/literal-positive-c-leaf/check.py @@ -0,0 +1,246 @@ +"""Author finite checks. Decoded arithmetic is confined to these oracles.""" +from pathlib import Path +import hashlib +import json +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import leaf as m + +CODE, ALPHABET = m.compile_leaf() + + +class ObservedTape(m.Tape): + def begin_call(self): + self.call_low = self.call_high = self.head + + def move(self, direction): + super().move(direction) + self.call_low = min(self.call_low, self.head) + self.call_high = max(self.call_high, self.head) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def gamma(n): + b = bin(n)[2:] + return '0'*(len(b)-1)+b + + +def header(f, r, p, s, w, cutoff): + return ''.join(gamma(n) for n in (f, r, p, s, w, cutoff)) + + +def signed(n, width): + require(-(1 << (width-1)) <= n < (1 << (width-1)), 'oracle signed fixture') + return format(n % (1 << width), '0'+str(width)+'b') + + +def encode(values, w): + return ''.join(signed(a, w)+signed(b, w) for a, b in values) + + +def multiply(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def weights(f): + result = [] + for x in range(1 << f): + c = (1, 0) + for j in range(f): + c = multiply(c, (1, -1 if x >> j & 1 else 1)) + result.append(c) + return result + + +def oracle(values, f, r, p, s, w): + """Direct tensor rows, not the executable butterfly or carry algorithm.""" + q, tail = 1 << f, (1 << (8*f))*s*r + require(len(values) == p*q*tail, 'oracle complete array') + coeffs, denominator = weights(f), 1 << f + out = [] + for outer in range(p): + for x in range(q): + for z in range(tail): + real = imag = 0 + for y in range(q): + a, b = multiply(coeffs[x ^ y], values[(outer*q+y)*tail+z]) + real += a + imag += b + require(real % denominator == imag % denominator == 0, + 'nonintegral tensor oracle result') + out.append((real//denominator, imag//denominator)) + return encode(out, w) + + +def caps(f, r, p, s, w, cutoff): + e = len(header(f, r, p, s, w, cutoff)) + n = p*s*r*(1 << (9*f)) + v = 2*n*w + up = s*r*(1 << (9*f-1)) + pre = p*(1 << (f-1)) + hi = max(pre, up, f, r, p, s, w) + return [e, v, v, v, 1, e, e, hi, f, r, p, s, w, + f.bit_length(), f.bit_length(), cutoff.bit_length(), cutoff.bit_length(), + pre, up, 2*up*w, 2*up*w, 2*up*w, 2*up*w, + w, w, w, w, w+2, v] + + +def packet(shape, word, origins=None, roomy=None): + origins = origins or tuple(5*i-83 for i in range(29)) + limits = roomy or caps(*shape) + tapes = [] + for i, (origin, limit) in enumerate(zip(origins, limits)): + cell = {origin-3: '1', origin-2: '|', origin+limit+1: '0', origin+limit+2: '|'} + if i < 2: + cell[origin-1] = '1' + tapes.append(ObservedTape(cell, origin)) + tapes[-1].begin_call() + for i, text in enumerate((header(*shape), word)): + tapes[i].cells.update({origins[i]+j: bit for j, bit in enumerate(text)}) + return tapes, origins + + +def run_case(shape, values, *, accept=True, code=CODE, change=None, tapes=None, origins=None): + f, r, p, s, w, cutoff = shape + word = encode(values, w) + if tapes is None: + tapes, origins = packet(shape, word) + for tape in tapes: + tape.begin_call() # Observation only; primitive low/high histories persist. + if change: + change(tapes, origins) + before = [dict(t.cells) for t in tapes] + owners = tuple(map(id, tapes)) + k0 = sum(t.high-t.low+1 for t in tapes[2:]) + cpu = m.Machine(code, tapes) + rejected = False + try: + cpu.run(1_000_000_000) + except ValueError as exc: + require(str(exc) == 'invalid scanned symbol', 'unexpected failure: '+str(exc)) + rejected = True + require(rejected != accept, 'acceptance mismatch') + require(tuple(map(id, tapes)) == owners, 'owner replaced') + require(tapes[0].cells == before[0], 'header changed') + if accept: + expected = oracle(values, f, r, p, s, w) + require(tapes[1].cells == before[1] | {origins[1]+j: bit for j, bit in enumerate(expected)}, + 'complete tensor result or public exterior mismatch') + require(all(t.head == u for t, u in zip(tapes, origins)), 'head not returned') + require(all(t.cells == before[i] for i, t in enumerate(tapes) if i != 1), + 'private window/exterior not restored') + e, v = len(header(*shape)), len(word) + require(cpu.steps <= 65536*(f*v+e+1), 'complete tariff exceeded') + for i, (tape, origin, cap) in enumerate(zip(tapes, origins, caps(*shape))): + require(tape.call_low >= origin-(i >= 2) and tape.call_high <= origin+cap, + 'proved frame cap exceeded') + require(sum(t.high-t.low+1 for t in tapes[2:]) <= k0+64*(v+e+1), + 'private backing envelope exceeded') + else: + require(tapes[1].cells == before[1], 'rejected call changed public DATA') + return cpu.steps + + +def authenticate(): + sources = json.loads((HERE/'SOURCES.json').read_text())['files'] + for pin in sources: + raw = (HERE/pin['local']).read_bytes() + require(len(raw) == pin['bytes'], 'source length') + require(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'source hash') + require(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == pin['blob'], + 'source Git blob') + for op, *args in CODE: + require(op in ('read', 'write', 'move', 'goto', 'halt'), 'nonliteral opcode') + if op in ('read', 'write', 'move'): + require(type(args[0]) is int and 0 <= args[0] < 29, 'tape range') + if op == 'move': + require(args[1] in (-1, 1), 'nonlocal movement') + if op == 'write': + require(args[1] in ALPHABET, 'nonfixed symbol') + if op == 'read': + require(set(args[1]) <= set(ALPHABET), 'read alphabet') + require(all(0 <= v < len(CODE) for v in args[1].values()), 'branch range') + if op == 'goto': + require(0 <= args[0] < len(CODE), 'fixed jump range') + return len(sources) + + +def repeated_history(): + shapes = [(1,2,1,1,4,3), (1,1,1,1,2,1), (1,2,1,1,4,3)] + roomy = [max(caps(*shape)[i] for shape in shapes) for i in range(29)] + tapes, origins = packet(shapes[0], encode([(1,-1)]*1024,4), roomy=roomy) + owners = tuple(map(id,tapes)) + prior = [t.high-t.low+1 for t in tapes] + history, steps = [], [] + for shape in shapes: + f,r,p,s,w,cutoff = shape + values = [(-2,-2) if w==2 else (1,-1)]*(p*s*r*(1 << (9*f))) + # Paid caller fixtures replace only public encodings. No private bank, + # primitive head or historical low/high observer is reset/replaced. + for i,text in enumerate((header(*shape),encode(values,w))): + for j in range(roomy[i]+1): + tapes[i].cells.pop(origins[i]+j,None) + tapes[i].cells.update({origins[i]+j:bit for j,bit in enumerate(text)}) + steps.append(run_case(shape,values,tapes=tapes,origins=origins)) + require(tuple(map(id,tapes))==owners, 'repeat replaced owner') + now = [t.high-t.low+1 for t in tapes] + require(all(a<=b for a,b in zip(prior,now)), 'history shrank or reset') + prior = now + history.append(sum(now[2:])) + require(history[0]==history[1]==history[2], 'reused bank incorrectly changed history') + return {'calls':3,'private_history':history,'steps':steps,'owner_inventory':29} + + +def main(): + sources = authenticate() + rng = random.Random(2026111204) + cases, steps = [], 0 + for w, value in ((2, (-2, -2)), (3, (3, 3)), (3, (-4, -4))): + shape = (1, 1, 1, 1, w, 1) + count = run_case(shape, [value]*512) + cases.append({'shape': list(shape), 'kind': 'constant signed endpoint', 'steps': count}) + steps += count + for shape in ((1, 2, 1, 1, 4, 1), (1, 1, 2, 1, 5, 3), (1, 1, 1, 2, 4, 2)): + f, r, p, s, w, cutoff = shape + values = [(2*rng.randrange(-1, 2), 2*rng.randrange(-1, 2)) + for _ in range(p*s*r*(1 << (9*f)))] + count = run_case(shape, values) + cases.append({'shape': list(shape), 'kind': 'dirty complete spectators and coefficients', 'steps': count}) + steps += count + cutoff = (1 << 2048)+17 + count = run_case((1, 1, 1, 1, 3, cutoff), [(1, -1)]*512) + cases.append({'shape': [1, 1, 1, 1, 3, '2049-bit threshold'], 'kind': 'binary cutoff', 'steps': count}) + steps += count + rejected = [] + bad = [(0, 0)]*512 + bad[-1] = (1, 0) + rejected.append(run_case((1, 1, 1, 1, 3, 1), bad, accept=False)) + bad = [(0, 0)]*512 + bad[255], bad[511] = (3, -3), (3, 3) + rejected.append(run_case((1, 1, 1, 1, 3, 1), bad, accept=False)) + rejected.append(run_case((2, 1, 1, 1, 3, 1), [], accept=False)) + rejected.append(run_case((1, 1, 1, 1, 1, 1), [(0, 0)]*512, accept=False)) + rejected.append(run_case((1, 1, 1, 1, 3, 1), [(0, 0)]*512, accept=False, + change=lambda t,o: t[1].cells.pop(o[1]+3071))) + rejected.append(run_case((1, 1, 1, 1, 3, 1), [(0, 0)]*512, accept=False, + change=lambda t,o: t[1].cells.__setitem__(o[1]+3072, '0'))) + reuse = repeated_history() + print(json.dumps({'status':'PASS_LITERAL_C_AUTHOR_BASE','seed':2026111204, + 'sources':sources,'locations':len(CODE),'tapes':29,'successes':cases, + 'successful_steps':steps,'rejections':len(rejected),'rejected_steps':sum(rejected), + 'repeated_history':reuse, + 'source_sha256':hashlib.sha256((HERE/'leaf.py').read_bytes()).hexdigest(), + 'table_sha256':hashlib.sha256(json.dumps([CODE,ALPHABET],sort_keys=True,separators=(',',':')).encode()).hexdigest(), + 'scope':'Complete physical f=1 packets; f>1 covered separately, not inferred from rank1.'},indent=2,sort_keys=True)) + + +if __name__ == '__main__': + main() + diff --git a/research/literal-positive-c-leaf/check_big.py b/research/literal-positive-c-leaf/check_big.py new file mode 100644 index 0000000000..0830f7012f --- /dev/null +++ b/research/literal-positive-c-leaf/check_big.py @@ -0,0 +1,130 @@ +"""Execute the actual m=9 table at f=2 with a separate dense C++ interpreter. + +The fixture and exact tensor oracle are outside the executing controller. +No reduced native dimension is substituted for the claimed table. +""" +from pathlib import Path +import hashlib +import json +import subprocess +import sys +import tempfile +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import check as c + + +def table_text(code): + numbers = {'_':0, '0':1, '1':2, '|':3} + rows = [str(len(code))] + for op, *a in code: + tape = value = 0 + targets = [-1]*4 + if op == 'read': + tag, tape = 0, a[0] + for symbol, target in a[1].items(): + targets[numbers[symbol]] = target + elif op == 'write': + tag, tape, value = 1, a[0], numbers[a[1]] + elif op == 'move': + tag, tape, value = 2, a[0], a[1] + elif op == 'goto': + tag, value = 3, a[0] + elif op == 'halt': + tag = 4 + else: + raise ValueError('unknown instruction') + rows.append(' '.join(map(str, (tag, tape, value, *targets)))) + return '\n'.join(rows)+'\n' + + +def invoke(tmp, executable, shape, values, code=c.CODE, accept=True): + word = c.encode(values, shape[4]) + program, packet, output = (tmp/n for n in ('program.txt','packet.txt','output.txt')) + program.write_text(table_text(code)) + origins = [64+2*i for i in range(29)] + packet.write_text(' '.join(map(str, origins))+'\n'+ + ' '.join(map(str, c.caps(*shape)))+'\n'+c.header(*shape)+'\n'+word+'\n') + started = time.monotonic() + result = subprocess.run([str(executable),str(program),str(packet),str(output)], + check=True,timeout=120,capture_output=True,text=True) + record = json.loads(result.stdout) + result_word = output.read_text() + c.require(record['accepted'] == accept, 'dense acceptance boundary') + for field in ('header_preserved','exteriors_preserved'): + c.require(record[field], 'dense CPU '+field) + if accept: + c.require(record['heads_returned'] and record['private_blank'], 'dense normal retirement') + c.require(record['data_writes']==len(word), 'dense complete public commit') + else: + c.require(record['data_writes']==0 and result_word==word, 'dense rejection changed DATA') + c.require(record['header_writes']==0, 'dense public header writes') + f = shape[0] + e = len(c.header(*shape)) + c.require(record['steps'] <= 65536*(f*len(word)+e+1), 'dense complete cost envelope') + c.require(record['private_history'] <= 27+64*(len(word)+e+1), 'dense private history envelope') + record['shape'] = list(shape) + record['input_bits'] = len(word) + record['output_sha256'] = hashlib.sha256(result_word.encode()).hexdigest() + # Wall times are metadata, not counted machine work or a complexity claim. + elapsed = time.monotonic()-started + return result_word, record, elapsed + + +def main(): + c.authenticate() + with tempfile.TemporaryDirectory(prefix='literal-C-full-') as directory: + tmp = Path(directory) + executable = tmp/'table_cpu' + subprocess.run(['c++','-std=c++17','-O2',str(HERE/'table_cpu.cpp'),'-o',str(executable)], + check=True,timeout=60,capture_output=True,text=True) + small_shape = (1,1,1,1,3,1) + small_values = [(3,3)]*512 + small, small_record, small_time = invoke(tmp,executable,small_shape,small_values) + c.require(small == c.oracle(small_values,*small_shape[:5]), 'dense f1 exact oracle') + python_steps = c.run_case(small_shape,small_values) + c.require(small_record['steps']==python_steps, 'two interpreters disagree on literal count') + shape = (2,1,1,1,5,2) + values = [(4*((17*i+(i>>8))%3-1), 4*((7*i+(i>>16))%3-1)) + for i in range(1 << 18)] + expected = c.oracle(values,*shape[:5]) + result, full, full_time = invoke(tmp,executable,shape,values) + c.require(result==expected, 'actual full m9 f2 tensor differs') + # This semantically complete mutant retains owner/cleanup behavior but + # implements only the first axis, exposing rank-one/f=1 conflation. + builder = c.m.Builder() + old = c.m.Builder + c.m.Builder = lambda: builder + try: + code, alphabet = c.m.compile_leaf() + finally: + c.m.Builder = old + c.require(code==c.CODE and alphabet==c.ALPHABET, 'label-capture graph drift') + broken = list(code) + broken[builder.labels['next_axis']] = ('goto',builder.labels['finish']) + wrong, mutant, mutant_time = invoke(tmp,executable,shape,values,tuple(broken)) + c.require(wrong != expected, 'skipped tensor-axis mutant survived') + endpoint_values = [(1 if i >> 16 in (0,3) else 0,0) for i in range(1 << 18)] + endpoint_shape = (2,1,1,1,2,2) + endpoint_expected = c.oracle(endpoint_values,*endpoint_shape[:5]) + c.require(endpoint_expected == c.encode([(1 if i >> 16 in (1,2) else 0,0) + for i in range(1 << 18)],2), + 'endpoint-only admission witness formula') + _, endpoint, endpoint_time = invoke(tmp,executable,endpoint_shape,endpoint_values,accept=False) + print(json.dumps({'status':'PASS_ACTUAL_M9_F2_LITERAL_C','program_sha256': + hashlib.sha256((HERE/'leaf.py').read_bytes()).hexdigest(), + 'table_sha256':hashlib.sha256(json.dumps([c.CODE,c.ALPHABET],sort_keys=True,separators=(',',':')).encode()).hexdigest(), + 'interpreter_sha256':hashlib.sha256((HERE/'table_cpu.cpp').read_bytes()).hexdigest(), + 'compiler_flags':['-std=c++17','-O2'],'f1_cross_interpreter':small_record, + 'actual_f2':full,'f2_one_axis_mutant':mutant,'f2_endpoint_only_reject':endpoint, + 'controls':['skip every axis after the first while preserving data length, owner, heads and private retirement'], + 'scope':'Actual fixed m=9 table, complete 262144-address f=2 array; no reduced dimension or record subsampling.'}, + indent=2,sort_keys=True)) + print('Wall seconds f1/full-f2/mutant/endpoint-reject:', + *[round(t,3) for t in (small_time,full_time,mutant_time,endpoint_time)],file=sys.stderr) + + +if __name__ == '__main__': + main() diff --git a/research/literal-positive-c-leaf/independent/DENSE-RESULT-OPTIMIZED.json b/research/literal-positive-c-leaf/independent/DENSE-RESULT-OPTIMIZED.json new file mode 100644 index 0000000000..c68ad22221 --- /dev/null +++ b/research/literal-positive-c-leaf/independent/DENSE-RESULT-OPTIMIZED.json @@ -0,0 +1 @@ +{"actual_dimension_cases": 7, "actual_f2_complete_success": false, "large_cutoff_bits": 2049, "locations": 6826, "mutations": ["wrong conjugate kernel", "rounding an odd numerator", "truncating signed overflow", "corrupt original-owner installation"], "private_history_span": 4298, "program_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", "rejections": 167, "smaller_dimension_fixtures": 267, "status": "PASS_INDEPENDENT_POSITIVE_C", "successes": 111, "successful_transitions": 9782553} diff --git a/research/literal-positive-c-leaf/independent/DENSE-RESULT.json b/research/literal-positive-c-leaf/independent/DENSE-RESULT.json new file mode 100644 index 0000000000..c68ad22221 --- /dev/null +++ b/research/literal-positive-c-leaf/independent/DENSE-RESULT.json @@ -0,0 +1 @@ +{"actual_dimension_cases": 7, "actual_f2_complete_success": false, "large_cutoff_bits": 2049, "locations": 6826, "mutations": ["wrong conjugate kernel", "rounding an odd numerator", "truncating signed overflow", "corrupt original-owner installation"], "private_history_span": 4298, "program_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", "rejections": 167, "smaller_dimension_fixtures": 267, "status": "PASS_INDEPENDENT_POSITIVE_C", "successes": 111, "successful_transitions": 9782553} diff --git a/research/literal-positive-c-leaf/independent/dense_check.py b/research/literal-positive-c-leaf/independent/dense_check.py new file mode 100644 index 0000000000..3a81a8a303 --- /dev/null +++ b/research/literal-positive-c-leaf/independent/dense_check.py @@ -0,0 +1,206 @@ +"""Independent dense local CPU and direct tensor-polynomial C oracle. +Prepared for CubeJerry with OpenAI assistance. Apache-2.0. +The author interpreter, tests and expected-output routine are not used. +""" +from pathlib import Path +import hashlib, importlib.util, json, sys + +def need(x, message): + if not x: raise AssertionError(message) + +class Rejected(Exception): pass + +SYMBOLS = '_01|' + +class CPU: + def __init__(self, tapes, capacity): + self.origin = [19+2*t for t in range(tapes)] + self.head = self.origin.copy() + self.rows = [bytearray(capacity) for _ in range(tapes)] + for t,o in enumerate(self.origin): + self.rows[t][o-6:o-2] = bytes((2,1,3,2)) + self.rows[t][-5:-1] = bytes((1,2,3,1)) + self.low = self.origin.copy(); self.high = self.origin.copy() + + def supply(self, fields): + need(self.head==self.origin, 'clean successful reuse') + for t,word in enumerate(fields): + row=self.rows[t]; o=self.origin[t] + row[o:-6]=bytes(len(row)-6-o) + row[o:o+len(word)] = bytes(SYMBOLS.index(c) for c in word) + row[o+len(word)+1:o+len(word)+5] = bytes((1,2,3,1)) + self.before = [r[:] for r in self.rows] + + def run(self, code, limit=120_000_000): + compiled=[]; nt=len(self.rows) + for ins in code: + op,*args=ins + if op=='read': + t,branches=args; need(0<=thi[t]:hi[t]=h[t] + elif op==3:pc=t + else:return steps,counts + raise AssertionError('bounded observer budget exhausted') + +def gamma(n): + b=format(n,'b');return '0'*(len(b)-1)+b + +def mul(a,b):return (a[0]*b[0]-a[1]*b[1],a[0]*b[1]+a[1]*b[0]) + +def weight(k,h): + z=(1,0) + for _ in range(k-h):z=mul(z,(1,1)) + for _ in range(h):z=mul(z,(1,-1)) + return z + +def oracle(values, shape, dimension): + """Each partial tensor is recomputed directly from the original values. + No butterfly recurrence or signed carry implementation is reused. + """ + f,r,P,S,w,cutoff=shape + if f>cutoff or w<2:return None + Q=1<>3))%3)-1)*(1<>2))%3)-1)*(1<=hist,'retained history');hist=h + controls=[] + def detect(broken,shape,values,label): + try:check(broken,shape,1,values) + except (AssertionError,Rejected):controls.append(label) + else:raise AssertionError('undetected mutation '+label) + original_rows=m.ROWS;m.ROWS=(original_rows[2],original_rows[3],original_rows[0],original_rows[1]) + wrong,_=m.compile_leaf();m.ROWS=original_rows + detect(wrong,(1,1,1,1,5,1),[(2,0),(0,0)],'wrong conjugate kernel') + broken=list(small);changed=0 + for i,ins in enumerate(small): + if ins[:2]==('read',m.NUM) and set(ins[2])=={'0','1'} and ins[2]['1']==len(small)-1: + broken[i]=('read',m.NUM,{'0':ins[2]['0'],'1':ins[2]['0']});changed+=1 + need(changed==4,'four exact divisibility gates') + detect(broken,(1,1,1,1,3,1),[(1,0),(0,0)],'rounding an odd numerator') + broken=list(small);changed=0 + for i,ins in enumerate(small): + if ins[:2]==('read',m.NUM) and len(ins[2])==1 and next(iter(ins[2])) in ('0','1'): + dest=next(iter(ins[2].values()));broken[i]=('read',m.NUM,{'0':dest,'1':dest});changed+=1 + need(changed==8,'eight signed fit branches') + detect(broken,(1,1,1,1,2,1),[(-2,-2),(-2,0)],'truncating signed overflow') + broken=list(small) + for i,ins in enumerate(small): + if ins[:2]==('write',m.DATA) and ins[2]=='1':broken[i]=('write',m.DATA,'0') + detect(broken,(1,1,1,1,5,1),[(2,0),(0,0)],'corrupt original-owner installation') + need(hashlib.sha256(path.read_bytes()).hexdigest()==digest,'source changed during review') + print(json.dumps({'status':'PASS_INDEPENDENT_POSITIVE_C','program_sha256':digest,'locations':len(actual), + 'actual_dimension_cases':actual_cases,'actual_f2_complete_success':False, + 'smaller_dimension_fixtures':fixtures,'successes':successes,'rejections':rejections, + 'successful_transitions':steps,'private_history_span':hist,'large_cutoff_bits':2049, + 'mutations':controls},sort_keys=True)) + +if __name__=='__main__':main() + diff --git a/research/literal-positive-c-leaf/independent/peer/RESULT-OPTIMIZED.json b/research/literal-positive-c-leaf/independent/peer/RESULT-OPTIMIZED.json new file mode 100644 index 0000000000..d7681d744b --- /dev/null +++ b/research/literal-positive-c-leaf/independent/peer/RESULT-OPTIMIZED.json @@ -0,0 +1,142 @@ +{ + "axis_cost": { + "exact_complete_axis_cost": "99*V + 153*N + 48*A + 16, before next-axis geometry or final commit", + "independent_local_transitions": 875232, + "isolated_axis_cost_cases": 27, + "scope": "Isolated guide-driven axis slices, including small generalized guide lengths; these are cost checks, not claims of complete selected m=9 packets." + }, + "component_lowering": { + "accepted_components": 8132, + "complete_component_cases": 17528, + "exact_successful_helper_cost": "43*w+57, excluding wrapper halt", + "independent_local_transitions": 4994452, + "mutants_detected": [ + "odd numerator incorrectly admitted", + "conjugate/wrong C signs", + "functionally unchanged helper cost drift" + ] + }, + "geometry": { + "axis_geometries": 432, + "full_integer_address_probes": 10224 + }, + "graph": { + "finite_carry_cases": 256, + "locations": 6826, + "table_and_alphabet_sha256": "ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9" + }, + "leaf_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", + "proof_sha256": "c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c", + "scope": "Source pins, full exact Walsh-spectral kernels through 8 axes, exact literal component helpers including all width-2 and width-3 inputs. Not full-packet all-f execution; root provides separate dense runtime review.", + "sources": [ + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "753a44f2b392d8a0297cb1324be396f246f69935", + "path": "research/current-coded-gaussian-leaf/README.md", + "sha256": "5554fdac912fcb92a7833a8b860f8d21962f78eb2a4087d3688f476b891db2f3" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "3479c700c9b68968106454e57993e9615cc6a821", + "path": "research/current-coded-gaussian-leaf/PROOF.md", + "sha256": "f01a2c81805eed7f6983d9928258100a00a7c8e6f2532bf10610c0883c7e972d" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "e98db470cdb8bfc49e9da86c39c0d6ae16e92716", + "path": "research/physical-gaussian-leaf/PROOF.md", + "sha256": "29ebd43146f921077f980a408915ecc3a5199a07fcdadc624a8282c06b0b8104" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "path": "research/shared-wire-split-composition/frozen/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "path": "research/shared-wire-split-composition/frozen/native_verify.py", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "74563a7867d9d762b6588f65362369668841bb3e", + "path": "research/shared-wire-split-composition/data/final.json.gz", + "sha256": "2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "98b35c89c8bd52637633aa78d506244bca8ec9e1", + "path": "docs/research/pr-intake-evidence/pr7000-application/check_native_catalogue.py", + "sha256": "6120e1ea1e07eeba757694d209437a38f121b0a377cc466889a30fa52c561472" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "path": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa", + "git_blob": "3ab6d0361f35038ffcdf0cf81a157f7a17b40e72", + "path": "research/selected-rank-control/controller_reference.py", + "sha256": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73" + }, + { + "commit": "8b549ca6557ccbb3017b104b27ea35051f990416", + "git_blob": "c6e87695340a12d76d8f4fc8fb9ae069d3ec6a47", + "path": "research/literal-layer-phase/phase.py", + "sha256": "9a360817b80e869398927f38a4f110de0b5a1f9620eeb23b19e166f112b83f23" + }, + { + "commit": "172f4535ce8dcff79f626410af845f757c1563be", + "git_blob": "46a43bf214d828aa972db66ad35e41b9cd07a964", + "path": "research/literal-native-quadratic-phase/PROOF.md", + "sha256": "55f0a575f618bf467d0e25a25802053455d701cee1f23fb8811a671a1bd59ff3" + } + ], + "spectral_tensors": [ + { + "axes": 1, + "component_row_l1": 2, + "sharp_denominator": 2 + }, + { + "axes": 2, + "component_row_l1": 2, + "sharp_denominator": 2 + }, + { + "axes": 3, + "component_row_l1": 4, + "sharp_denominator": 4 + }, + { + "axes": 4, + "component_row_l1": 4, + "sharp_denominator": 4 + }, + { + "axes": 5, + "component_row_l1": 8, + "sharp_denominator": 8 + }, + { + "axes": 6, + "component_row_l1": 8, + "sharp_denominator": 8 + }, + { + "axes": 7, + "component_row_l1": 16, + "sharp_denominator": 16 + }, + { + "axes": 8, + "component_row_l1": 16, + "sharp_denominator": 16 + } + ], + "status": "PASS_SOURCE_SPECTRAL_HELPER_REVIEW" +} diff --git a/research/literal-positive-c-leaf/independent/peer/RESULT.json b/research/literal-positive-c-leaf/independent/peer/RESULT.json new file mode 100644 index 0000000000..d7681d744b --- /dev/null +++ b/research/literal-positive-c-leaf/independent/peer/RESULT.json @@ -0,0 +1,142 @@ +{ + "axis_cost": { + "exact_complete_axis_cost": "99*V + 153*N + 48*A + 16, before next-axis geometry or final commit", + "independent_local_transitions": 875232, + "isolated_axis_cost_cases": 27, + "scope": "Isolated guide-driven axis slices, including small generalized guide lengths; these are cost checks, not claims of complete selected m=9 packets." + }, + "component_lowering": { + "accepted_components": 8132, + "complete_component_cases": 17528, + "exact_successful_helper_cost": "43*w+57, excluding wrapper halt", + "independent_local_transitions": 4994452, + "mutants_detected": [ + "odd numerator incorrectly admitted", + "conjugate/wrong C signs", + "functionally unchanged helper cost drift" + ] + }, + "geometry": { + "axis_geometries": 432, + "full_integer_address_probes": 10224 + }, + "graph": { + "finite_carry_cases": 256, + "locations": 6826, + "table_and_alphabet_sha256": "ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9" + }, + "leaf_sha256": "bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744", + "proof_sha256": "c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c", + "scope": "Source pins, full exact Walsh-spectral kernels through 8 axes, exact literal component helpers including all width-2 and width-3 inputs. Not full-packet all-f execution; root provides separate dense runtime review.", + "sources": [ + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "753a44f2b392d8a0297cb1324be396f246f69935", + "path": "research/current-coded-gaussian-leaf/README.md", + "sha256": "5554fdac912fcb92a7833a8b860f8d21962f78eb2a4087d3688f476b891db2f3" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "3479c700c9b68968106454e57993e9615cc6a821", + "path": "research/current-coded-gaussian-leaf/PROOF.md", + "sha256": "f01a2c81805eed7f6983d9928258100a00a7c8e6f2532bf10610c0883c7e972d" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "e98db470cdb8bfc49e9da86c39c0d6ae16e92716", + "path": "research/physical-gaussian-leaf/PROOF.md", + "sha256": "29ebd43146f921077f980a408915ecc3a5199a07fcdadc624a8282c06b0b8104" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "path": "research/shared-wire-split-composition/frozen/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "path": "research/shared-wire-split-composition/frozen/native_verify.py", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "74563a7867d9d762b6588f65362369668841bb3e", + "path": "research/shared-wire-split-composition/data/final.json.gz", + "sha256": "2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "98b35c89c8bd52637633aa78d506244bca8ec9e1", + "path": "docs/research/pr-intake-evidence/pr7000-application/check_native_catalogue.py", + "sha256": "6120e1ea1e07eeba757694d209437a38f121b0a377cc466889a30fa52c561472" + }, + { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "path": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "commit": "9dfe6747b8553fd11b408f2b045c5954ef1e6eaa", + "git_blob": "3ab6d0361f35038ffcdf0cf81a157f7a17b40e72", + "path": "research/selected-rank-control/controller_reference.py", + "sha256": "e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73" + }, + { + "commit": "8b549ca6557ccbb3017b104b27ea35051f990416", + "git_blob": "c6e87695340a12d76d8f4fc8fb9ae069d3ec6a47", + "path": "research/literal-layer-phase/phase.py", + "sha256": "9a360817b80e869398927f38a4f110de0b5a1f9620eeb23b19e166f112b83f23" + }, + { + "commit": "172f4535ce8dcff79f626410af845f757c1563be", + "git_blob": "46a43bf214d828aa972db66ad35e41b9cd07a964", + "path": "research/literal-native-quadratic-phase/PROOF.md", + "sha256": "55f0a575f618bf467d0e25a25802053455d701cee1f23fb8811a671a1bd59ff3" + } + ], + "spectral_tensors": [ + { + "axes": 1, + "component_row_l1": 2, + "sharp_denominator": 2 + }, + { + "axes": 2, + "component_row_l1": 2, + "sharp_denominator": 2 + }, + { + "axes": 3, + "component_row_l1": 4, + "sharp_denominator": 4 + }, + { + "axes": 4, + "component_row_l1": 4, + "sharp_denominator": 4 + }, + { + "axes": 5, + "component_row_l1": 8, + "sharp_denominator": 8 + }, + { + "axes": 6, + "component_row_l1": 8, + "sharp_denominator": 8 + }, + { + "axes": 7, + "component_row_l1": 16, + "sharp_denominator": 16 + }, + { + "axes": 8, + "component_row_l1": 16, + "sharp_denominator": 16 + } + ], + "status": "PASS_SOURCE_SPECTRAL_HELPER_REVIEW" +} diff --git a/research/literal-positive-c-leaf/independent/peer/REVIEW.md b/research/literal-positive-c-leaf/independent/peer/REVIEW.md new file mode 100644 index 0000000000..039c5e2f91 --- /dev/null +++ b/research/literal-positive-c-leaf/independent/peer/REVIEW.md @@ -0,0 +1,221 @@ +# Independent review of the literal positive C leaf + +**Disposition: accepted for the stated packed, positive, all-column direct-leaf +interface.** This review establishes no complete MOVE, old-format bridge, new +kappa, or unconditional multiplication theorem. Root's separately written +full-packet runtime review is a separate receipt. + +Reviewed at canonical base `e54523517d0f03e58352e647c403a5af3e525a57`: + +- `leaf.py`: `bb46c1a55f1119957a52cd61f2cd957f3f7ad1e9b818c54a852bde09a0773744`. +- `PROOF.md`: `c99157c3c43ae490b858cdbce04d85f3661ca5d9752770506d18ec4876c4ed6c`. +- Fixed graph and alphabet, canonical sorted compact JSON: + `ac8f5e05a4e0264e94eacb7887b568bead2cce5583607b5047ac560aaf434dc9`. + +The reviewer was the separately executing worker B, with OpenAI assistance, +working for Jerry Chen / @CubeJerry. No author science file was edited. Two +requested clarifications were applied by the author: the suffix-stream caps +use the maximum `U*`, and private-owner versus all-owner historical accounting +is explicit. The code and table did not change. The suggested final-only +integrality counterexample was also included before the reviewed proof froze. + +## 1. Exact source and admission + +I checked all eleven retained source files against their byte hashes and the +actual Git objects at each specified `commit:path`; `check.py` records the +objects in its receipt. In particular, the selected native artifact is the +current #7000 word, not the historical #6030 word used by #6967. Its event +24472 is exactly `["MOVE",415,3,99,false]`, with frames `[]` and `[239]`. +The retained source lowers the rank-one child as right monomial, positive +`fourier(...,range(1))`, then left monomial. `cgate` defaults to positive sign. +Thus the central matrix is + +`C = [[1+i,1-i],[1-i,1+i]]/2`. + +The denominator and its sign are essential. Neither the full source MOVE nor +one of its monomial factors is identified with this central operation. The +rank is one coordinate in each column. With f columns, that means f separate +C factors on the f bits of coordinate zero. + +The packed input is exactly `[P] x [2^f]^9 x [S]`, with r Gaussian w-bit MSB +pairs at each address. The first five Gamma fields are those of the published +literal phase package at `172f4535ce8dcff79f626410af845f757c1563be`; a sixth +Gamma field supplies the cutoff. The old #6967 twenty-three-field, coded-LSB +ABI is different and remains an explicit caller obligation. The theorem +requires positive f,r,P,S,cutoff, w>=2, actual f<=cutoff, complete payload, and +the private blank-window/owner premises. No host-origin, stride or coefficient +provider is supplied by the checker or smuggled into the program. + +## 2. Numerical invariant and all-column domain + +For an independent arithmetic oracle I used the Walsh spectral formula + +`C = H diag(1,i) H / 2`, where `H=[[1,1],[1,-1]]`. + +The k-axis coefficient at row y, column x is consequently + +`2^-k sum_z (-1)^((x xor y) dot z) i^popcount(z)`. + +This oracle uses exact rational Gaussian coordinates and a frequency sum. It +does not use the author's product-of-Gaussian-factors oracle, butterfly loop, +or expected-value implementation. It independently derives the four scalar +numerator rows and checks the exact kernels for k=1 through 8, including row +unitarity and the constant-fibre eigenvalue one. + +Universally, with pi=1+i, the equivalent identity +`C=pi^-1 [[i,1],[1,i]]` makes every k-factor entry a Gaussian unit times +`pi^-k`. At k=2s exactly one coordinate of each entry has magnitude 2^-s; +at k=2s+1 both have magnitude 2^-(s+1). Hence the common binary denominator +is sharply `2^ceil(k/2)` and a real-component row has l1 norm +`2^ceil(k/2)`. This proves the inherited sufficient reserve/headroom condition +for every completed prefix, rather than treating finite k checks as the +universal proof. These statements are credited #3091/predecessor results, +not new mathematics in this package. + +The actual accepting domain is broader: each executed axis must produce +integral components fitting the signed width. A final tensor endpoint alone +does not imply this. At f=2, the real fibre `[1,0,0,1]` has exact final output +`[0,1,1,0]`, but its first low-bit pairs have half-integral output. Correct +execution rejects it before a public write. Constant fibres with every real +and imaginary component equal to `-2^(w-1)` are fixed by C and are accepted; +this rules out implementations that negate the minimum value in an +insufficiently wide temporary. + +For the scalar lowering, let the original component bound be L=2^(w-1). +Each row has three positive terms and one negative term, so its exact +numerator belongs to `[-4L+1,4L-3]`. The finite carry set {-1,0,1,2} is closed +under the emitted digit recurrence. The written digit identity gives an +induction for every width. Two sign-extension steps produce a w+2-bit +representative in a range that identifies it uniquely with the actual +numerator. Testing its low bit gives exact divisibility by two. Equality of +the two highest remaining sign bits is exactly signed w-bit fit of the half. +The emitted MSB bits therefore represent the intended result, including the +most-negative endpoint. The private unhalved numerator is never restricted +to w bits. + +## 3. Physical geometry, ordering and lifecycle + +At axis j, the two halves within a prefix have + +`A_j=P 2^(f-1-j)`, `U_j=Sr 2^(8f+j)`, and `2 A_j U_j=N`. + +Writing a physical coefficient slot as +`(outer*2^f + coordinate)*tail + rest`, with `tail=Sr2^(8f)`, replacing the +half side maps it precisely to the slot with `coordinate xor 2^j` and the +same outer/rest values. This is an exact integer identity. The independent +checker probes it in 432 axis geometries and 10,224 full-integer addresses, +including first/last/interior spectator positions; these are checks of that +identity, not an exhaustive claim over arbitrary inputs. + +The encoded construction doubles U eight times per F mark and P f-1 times. +Each subsequent axis doubles U and halves an even A, and F advances exactly +once. This proves the f-loop and its low-bit-first order without treating +rank one as f=1. Splitting two whole suffixes, operating corresponding +Gaussian pairs, and merging left then right preserves every spectator and +coefficient position. The target bank is complete before either bank is +rewound and MODE changes. No payload address is computed by the controller. + +The original DATA is cloned and returned before any numerical work. The +clone checks exactly V binary cells and then a blank. All exactness and +range failures happen in private storage, before the final commit. Width +and cutoff failures happen earlier. Thus the public DATA and HEADER remain +unchanged on the stated failures. Private cleanup and head return after +failure are expressly absent; I do not infer a retry contract from public +atomicity. On success the bank/suffix/component induction gives complete +retirement, original-owner DATA installation, and every original head. The +commit has no unverified numerical branch: its source is an already proved +complete binary bank. + +## 4. Independently counted full work and backing + +I counted the actual emitted local instructions, including reads, jumps, +rewinds and halt. Important exact prices (without an artificial wrapper +halt) are: + +| Operation | Cost | +| --- | --- | +| Successful scalar `c_component` | `43w+57` | +| One complete half load of U coefficients | `28Uw+14U+7` | +| One complete prefix, including both loads, all arithmetic, merges and local returns | `372Uw+306U+45` | +| One complete axis, through the branch selecting finish/next-axis | `99V+153N+48A+16` | +| Next-axis geometry update and jump | `47U+15A+33` | +| Initial complete source clone and return | `20V+14N+14A+11` | +| Commit itself, including trace return and bank return | `16V+7` | + +The checker independently executes isolated component graphs and 27 isolated +axis slices to confirm the exact counts. The small axis slices use arbitrary +positive guide lengths to test the subroutine census; they are explicitly not +claimed to be complete selected nine-coordinate arrays. The exact algebra +of these counts follows from the fixed loops and is independent of payload +values whenever the call succeeds. + +For w>=2, N<=V/4 and A,U<=N/2. A complete axis plus its possible geometry +update is therefore at most `151V+49`, well inside the author's allowance +`8192(V+1)`. The separately verified unary helper prices bound all initial +geometric sums. Gamma conversion for the first five values is bounded by +the sum of represented values, each <=V; the cutoff is never converted to +unary. Its binary acquisition, length comparison and cleanup cost O(E), +even when its value is arbitrarily larger than V. These observations pay +header repetition, copy, helper scans, source clone, all axes, public commit +and cleanup within the stated `65536(fV+E+1)` envelope. This is a direct-leaf +bill; the old-codec bridge, input transport and nonleaf work remain outside +it and must be charged by a caller. + +I checked the per-role maximum-capacity argument. In particular DOUBLE never +exceeds the largest final guide; each of LEFT/RIGHT/LOUT/ROUT has cap +`2wU*`, and all component/NUM banks have fixed roles. There are twenty +volume-bounded roles, six header-bounded roles and MODE. Including endpoints +and guards gives `20V+6E+57`. This bounds new visits, not total history after +erasure. For private owners the total is previous private history plus this +increment. For all 29 owners, adding at most V+E+2 public positions still +fits the same conservative `64(V+E+1)` envelope, with the full prior source +and opaque history included in K0. Repeated calls require per-role history +unions/maxima, not a maximum current aggregate volume. Relocated entry +origins also require their actual transport corridors. The corrected proof +states these distinctions explicitly. + +## 5. Independent finite evidence and controls + +`check.py` imports the frozen compiler only to obtain its local instructions; +it uses its own CPU for the reviewed helper graphs and uses the exact +spectral oracle above for expected arithmetic. It never imports the author +checker or calls the author's `Machine`. It checks: + +- All 17,408 scalar-row instances from every four-component input at widths + two and three, plus 120 wide endpoint instances through width 2,048. +- 17,528 total component cases, 8,132 accepts, and 4,994,452 independently + interpreted local transitions, including exact successful cost and private + numerator retirement. +- Twenty-seven complete axis cost slices, with 875,232 local transitions, + target/input-bank retirement and returned local heads. +- The fixed 6,826-location/29-tape/four-symbol local language, all 256 finite + carry branches, and absence of unary value expansion in the cutoff decoder. +- All eleven exact Git source bindings in this run. + +Three changed local programs are detected: accepting an odd numerator, +using conjugated/wrong C signs, and a functionally unchanged extra instruction +that violates the exact helper cost census. The latter is a census control, +not a claim that one extra instruction violates the generous asymptotic +budget. Root independently checks full packet execution; the author also +reports a genuinely complete f=2 run. Those are distinct from this review's +helper and universal-proof methods. + +Reproduce from the package root after these artifacts are retained there: + +```sh +python -I -W error -B independent/peer/check.py . +python -I -O -W error -B independent/peer/check.py . +``` + +For this run, replace the script path with `reviews/c4-peer/check.py` and +pass `worker-c4/research/literal-positive-c-leaf`. Normal and optimized receipts +must agree. Git-object authentication is repeated when the shared repository +objects are available; portable execution without that checkout still checks +all retained source byte pins and the frozen science/graph identities. The +saved receipt records the actual authenticated Git objects from this review. + +The remaining obligations are the ones the package lists: actual full source +MOVE composition, both surrounding monomials and placement, old-format +conversion, cutoff/precision admission, caller lifecycle requirements, +nonleaf tariffs and the five global foundational assumptions. None is +silently supplied by this acceptance. diff --git a/research/literal-positive-c-leaf/independent/peer/check.py b/research/literal-positive-c-leaf/independent/peer/check.py new file mode 100644 index 0000000000..ed50bd90ef --- /dev/null +++ b/research/literal-positive-c-leaf/independent/peer/check.py @@ -0,0 +1,388 @@ +#!/usr/bin/env python3 +"""Independent source, spectral arithmetic, local-carry and cost review. + +Prepared for Jerry Chen / CubeJerry with OpenAI assistance. Apache-2.0. +This does not import the author's test oracle or full-packet simulator. +""" +from pathlib import Path +import ast +from fractions import Fraction +import gzip +import hashlib +import importlib.util +import itertools +import json +import subprocess +import sys + +CANDIDATE = Path(__file__).resolve().parents[2] +DEFAULT = CANDIDATE if (CANDIDATE/'leaf.py').is_file() else CANDIDATE/'worker-c4/research/literal-positive-c-leaf' +PACKAGE = Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else DEFAULT +ROOT = Path('/workspace/scratch/be42ab5b7196/source') + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def module(path, name): + spec = importlib.util.spec_from_file_location(name, path) + value = importlib.util.module_from_spec(spec) + sys.modules[name] = value + spec.loader.exec_module(value) + return value + + +def mul(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def spectral_row(k): + """Walsh spectral diagonal i^popcount, not pair butterflies/products.""" + size = 1 << k + roots = ((1, 0), (0, 1), (-1, 0), (0, -1)) + ans = [] + for h in range(size): + a = b = 0 + for frequency in range(size): + x, y = roots[frequency.bit_count() % 4] + sign = -1 if (frequency & h).bit_count() % 2 else 1 + a += sign*x + b += sign*y + ans.append((Fraction(a, size), Fraction(b, size))) + return ans + + +PAIR_ROW = spectral_row(1) + + +def pair_fields(values): + z = ((values[0], values[1]), (values[2], values[3])) + out = [] + for y in (0, 1): + a = b = Fraction(0) + for x in (0, 1): + u, v = mul(PAIR_ROW[x ^ y], z[x]) + a += u + b += v + out.extend((a, b)) + return tuple(out) + + +def encode(n, w): + return format(n % (1 << w), '0'+str(w)+'b') + + +class CPU: + """Sparse dictionary state, separately written local graph interpreter.""" + def __init__(self, program, tapes): + self.program = program + self.cells = tapes + self.positions = [0]*len(tapes) + self.low = [0]*len(tapes) + self.high = [0]*len(tapes) + self.pc = 0 + self.steps = 0 + self.stopped = False + self.rejected = False + + def run(self, bound, stop_pc=None): + while not self.stopped and not self.rejected and self.pc != stop_pc: + require(self.steps < bound, 'independent helper budget') + insn = self.program[self.pc] + self.steps += 1 + opcode = insn[0] + self.pc += 1 + if opcode == 'goto': + self.pc = insn[1] + elif opcode == 'halt': + self.stopped = True + elif opcode == 'move': + t, delta = insn[1:] + self.positions[t] += delta + self.low[t] = min(self.low[t], self.positions[t]) + self.high[t] = max(self.high[t], self.positions[t]) + elif opcode == 'write': + t, symbol = insn[1:] + if symbol == '_': + self.cells[t].pop(self.positions[t], None) + else: + self.cells[t][self.positions[t]] = symbol + elif opcode == 'read': + t, branches = insn[1:] + symbol = self.cells[t].get(self.positions[t], '_') + target = branches.get(symbol) + if target is None: + self.rejected = True + else: + self.pc = target + else: + raise ValueError('unexpected local opcode') + return self + + +def helper_graph(m, signs): + builder = m.Builder() + m.c_component(builder, signs, m.LOUT) + builder.op('halt') + builder.mark('reject') + builder.op('read', m.HEADER, {}) + return builder.finish(('_', '0', '1', '|'))[0] + + +def helper_case(m, code, row_index, w, numbers, check_cost=True): + tapes = [{-1: '|'} for _ in range(29)] + for t, n in zip(m.INPUTS, numbers): + tapes[t].update(enumerate(encode(n, w))) + tapes[m.WIDTH].update((j, '1') for j in range(w)) + before = [dict(x) for x in tapes] + expected = pair_fields(numbers)[row_index] + ok = expected.denominator == 1 and -(1 << (w-1)) <= expected < (1 << (w-1)) + cpu = CPU(code, tapes).run(1000*(w+1)) + require(cpu.stopped == ok and cpu.rejected != ok, 'spectral helper acceptance') + if ok: + output = ''.join(cpu.cells[m.LOUT].get(j, '_') for j in range(w)) + require(output == encode(int(expected), w), 'spectral helper value') + require(cpu.cells[m.LOUT] == {-1: '|', **dict(enumerate(output))}, 'helper output extent') + require(all(cpu.cells[t] == before[t] for t in range(29) if t != m.LOUT), 'helper borrow/NUM retirement') + require(all(x == (w if t == m.LOUT else 0) for t, x in enumerate(cpu.positions)), 'helper head return') + require(cpu.low[m.NUM] == -1 and cpu.high[m.NUM] == w+2, 'literal numerator width') + if check_cost: + require(cpu.steps == 43*w+58, 'exact component tariff') + else: + require(cpu.cells[m.LOUT] == before[m.LOUT], 'failed component emitted output') + return cpu.steps, ok + + +def spectral_checks(): + report = [] + for k in range(1, 9): + row = spectral_row(k) + denom = max(x.denominator for pair in row for x in pair) + norm = sum(abs(a)+abs(b) for a, b in row) + require(denom == 1 << ((k+1)//2), 'sharp tensor denominator') + require(norm == 1 << ((k+1)//2), 'component row norm') + require(sum(a*a+b*b for a, b in row) == 1, 'unitary kernel row') + require(tuple(sum(v[part] for v in row) for part in (0, 1)) == (1, 0), 'constant-fibre eigenvalue') + report.append({'axes': k, 'sharp_denominator': denom, 'component_row_l1': int(norm)}) + # Final exactness is strictly weaker than successive-axis exactness. + witness = (1, 0, 0, 1) + row = spectral_row(2) + final = [] + for y in range(4): + final.append(tuple(sum(row[x ^ y][part]*witness[x] for x in range(4)) for part in (0, 1))) + require(final == [(0, 0), (1, 0), (1, 0), (0, 0)], 'final-only witness') + require(pair_fields((1, 0, 0, 0))[0].denominator == 2, 'first prefix is inexact') + return report + + +def geometry_checks(): + count = 0 + records = 0 + for f, p, s, r in itertools.product(range(1, 9), (1, 2, 5), (1, 3), (1, 2)): + tail = (1 << (8*f))*s*r + n = p*(1 << f)*tail + for j in range(f): + prefix = p*(1 << (f-1-j)) + suffix = s*r*(1 << (8*f+j)) + require(2*prefix*suffix == n, 'axis census') + if j+1 < f: + require(prefix % 2 == 0, 'exact prefix halving') + # Algebraic probes of full physical slots, including interiors and both ends. + for outer in (0, p-1): + for coordinate in sorted({0, (1 << f)-1, 1 << j, ((1 << f)-1) ^ (1 << j)}): + for rest in sorted({0, tail//2, tail-1}): + physical = (outer*(1 << f)+coordinate)*tail+rest + block, within = divmod(physical, 2*suffix) + side, offset = divmod(within, suffix) + mate = block*2*suffix+(1-side)*suffix+offset + target = (outer*(1 << f)+(coordinate ^ (1 << j)))*tail+rest + require(mate == target, 'physical coefficient pairing') + records += 1 + count += 1 + return {'axis_geometries': count, 'full_integer_address_probes': records} + + +def sources(): + pins = json.loads((PACKAGE/'SOURCES.json').read_text())['files'] + records = [] + for pin in pins: + data = (PACKAGE/pin['local']).read_bytes() + require(len(data) == pin['bytes'] and sha(data) == pin['sha256'], 'retained source bytes') + # Independent Git identity is optional after relocation without repository objects. + record = {'path': pin['path'], 'commit': pin['commit'], 'sha256': sha(data)} + if ROOT.exists(): + obj = subprocess.check_output(['git', '-C', str(ROOT), 'rev-parse', pin['commit']+':'+pin['path']], text=True).strip() + require(obj == pin['blob'], 'actual commit/path object') + raw = subprocess.check_output(['git', '-C', str(ROOT), 'cat-file', 'blob', obj]) + require(raw == data, 'actual Git source bytes') + record['git_blob'] = obj + records.append(record) + word = json.loads(gzip.decompress((PACKAGE/'reference/selected-native.json.gz').read_bytes())) + require(word['program'][24472] == ['MOVE', 415, 3, 99, False], 'actual selected occurrence') + require(word['frames'][3] == [] and word['frames'][99] == [239], 'actual selected frame edge') + src = (PACKAGE/'reference/clifford_exact.py').read_text() + require("def cgate(n,q,sgn=1):" in src, 'source positive C default') + require('out=out.then(cgate(n,1<=budget: raise ValueError('finite verifier budget') + self.step() + return self + +def initial_tapes(width,origins=(0,0,0),ancestor=('0','1','t0','_','|','0')): + if width<1: raise ValueError('positive width') + u,c,p=origins + return [Tape({u-1:MARK,**{u+i:ONE for i in range(width)}},u),Tape({c-1:MARK},c), + Tape({p-1:MARK,**{p-2-i:s for i,s in enumerate(ancestor) if s!=BLANK}},p)] diff --git a/research/literal-positive-c-leaf/leaf.py b/research/literal-positive-c-leaf/leaf.py new file mode 100644 index 0000000000..bdcc80cbd8 --- /dev/null +++ b/research/literal-positive-c-leaf/leaf.py @@ -0,0 +1,564 @@ +"""Literal positive rank-one Gaussian C tensor leaf on a packed m=9 field. + +Prepared for Jerry Chen / CubeJerry with substantial OpenAI assistance. +Apache-2.0. C arithmetic and tensor algebra are credited #3091 predecessors. +Only fixed local instructions execute; encoded inputs do not specialize code. +""" +from pathlib import Path +import hashlib +import sys + +HERE = Path(__file__).resolve().parent +MACHINE = HERE / 'inputs' / 'controller_reference.py' +EXPECTED_MACHINE = 'e664a748e6b6797d4b60f60a7a7dd68b59a5608acf56b9c5d8b466f363755f73' +if hashlib.sha256(MACHINE.read_bytes()).hexdigest() != EXPECTED_MACHINE: + raise ValueError('frozen literal machine source drift') +sys.path.insert(0, str(MACHINE.parent)) +from controller_reference import Builder, Machine, Tape, BLANK, ONE, MARK + +(HEADER, DATA, A, B, MODE, HTRACE, LENGTH, DOUBLE, F, R, P, S, WIDTH, + FBIN, FLEN, TBIN, TLEN, PREFIX, SUFFIX, LEFT, RIGHT, LOUT, ROUT, + AR, AI, BR, BI, NUM, DTRACE) = range(29) +PRIVATE = tuple(range(2, 29)) +BITS = ('0', ONE) +INPUTS = (AR, AI, BR, BI) +ROWS = ((1, -1, 1, 1), (1, 1, -1, 1), + (1, 1, 1, -1), (-1, 1, 1, 1)) +NATIVE_DIMENSION = 9 + + +def fresh(a, stem): + a.serial += 1 + return stem + str(a.serial) + + +def clear(a, tape, symbols=(ONE,)): + k = fresh(a, 'clear') + a.mark(k) + a.op('read', tape, {s: k+'bit' for s in symbols} | {BLANK: k+'done'}) + a.mark(k+'bit') + a.op('write', tape, BLANK) + a.op('move', tape, 1) + a.op('goto', k) + a.mark(k+'done') + a.rewind(tape, (BLANK,)) + + +def unary_copy(a, source, target, *, repeat=1, extra=0, erase=False): + k = fresh(a, 'copy') + a.mark(k) + a.op('read', source, {ONE: k+'bit', BLANK: k+'done'}) + a.mark(k+'bit') + for _ in range(repeat): + a.op('write', target, ONE) + a.op('move', target, 1) + if erase: + a.op('write', source, BLANK) + a.op('move', source, 1) + a.op('goto', k) + a.mark(k+'done') + for _ in range(extra): + a.op('write', target, ONE) + a.op('move', target, 1) + a.rewind(source, (BLANK,) if erase else (ONE,)) + a.rewind(target, (ONE,)) + + +def trace_return(a, tape, trace): + k = fresh(a, 'return') + a.op('move', trace, -1) + a.mark(k) + a.op('read', trace, {ONE: k+'bit', MARK: k+'done'}) + a.mark(k+'bit') + a.op('write', trace, BLANK) + a.op('move', trace, -1) + a.op('move', tape, -1) + a.op('goto', k) + a.mark(k+'done') + a.op('move', trace, 1) + + +def header_step(a): + a.op('write', HTRACE, ONE) + a.op('move', HTRACE, 1) + a.op('move', HEADER, 1) + + +def gamma(a, target, capture=None): + """Unary decode for parameters bounded by the actual field volume.""" + k = fresh(a, 'gamma') + a.mark(k+'prefix') + a.op('read', HEADER, {'0': k+'zero', ONE: k+'one'}) + a.mark(k+'zero') + a.op('write', LENGTH, ONE) + a.op('move', LENGTH, 1) + header_step(a) + a.op('goto', k+'prefix') + a.mark(k+'one') + header_step(a) + a.op('write', target, ONE) + if capture: + for tape, bit in ((capture[0], ONE), (capture[1], ONE)): + a.op('write', tape, bit) + a.op('move', tape, 1) + a.op('move', LENGTH, -1) + a.mark(k+'tail') + a.op('read', LENGTH, {ONE: k+'tailbit', MARK: k+'done'}) + a.mark(k+'tailbit') + a.op('write', LENGTH, BLANK) + a.op('read', HEADER, {str(b): k+'digit'+str(b) for b in (0, 1)}) + for bit in (0, 1): + a.mark(k+'digit'+str(bit)) + unary_copy(a, target, DOUBLE, repeat=2, extra=bit) + clear(a, target) + unary_copy(a, DOUBLE, target, erase=True) + if capture: + for tape, symbol in ((capture[0], str(bit)), (capture[1], ONE)): + a.op('write', tape, symbol) + a.op('move', tape, 1) + header_step(a) + a.op('move', LENGTH, -1) + a.op('goto', k+'tail') + a.mark(k+'done') + a.op('move', LENGTH, 1) + if capture: + a.rewind(capture[0], BITS) + a.rewind(capture[1], (ONE,)) + + +def gamma_binary(a): + """Keep cutoff in binary: its represented value can exceed V arbitrarily.""" + k = fresh(a, 'threshold') + a.mark(k+'prefix') + a.op('read', HEADER, {'0': k+'zero', ONE: k+'one'}) + a.mark(k+'zero') + a.op('write', LENGTH, ONE) + a.op('move', LENGTH, 1) + header_step(a) + a.op('goto', k+'prefix') + a.mark(k+'one') + a.op('write', TBIN, ONE) + a.op('move', TBIN, 1) + a.op('write', TLEN, ONE) + a.op('move', TLEN, 1) + header_step(a) + a.op('move', LENGTH, -1) + a.mark(k+'tail') + a.op('read', LENGTH, {ONE: k+'read', MARK: k+'done'}) + a.mark(k+'read') + a.op('write', LENGTH, BLANK) + a.op('read', HEADER, {str(b): k+str(b) for b in (0, 1)}) + for bit in ('0', ONE): + a.mark(k+bit) + a.op('write', TBIN, bit) + a.op('move', TBIN, 1) + a.op('write', TLEN, ONE) + a.op('move', TLEN, 1) + header_step(a) + a.op('move', LENGTH, -1) + a.op('goto', k+'tail') + a.mark(k+'done') + a.op('move', LENGTH, 1) + a.rewind(TBIN, BITS) + a.rewind(TLEN, (ONE,)) + + +def cutoff_guard(a): + k = fresh(a, 'compare') + a.mark(k+'length') + a.op('read', FLEN, {ONE: k+'fmore', BLANK: k+'fend'}) + a.mark(k+'fmore') + a.op('read', TLEN, {ONE: k+'step', BLANK: 'reject'}) + a.mark(k+'step') + a.op('move', FLEN, 1) + a.op('move', TLEN, 1) + a.op('goto', k+'length') + a.mark(k+'fend') + a.op('read', TLEN, {ONE: k+'done', BLANK: k+'equal_length'}) + a.mark(k+'equal_length') + a.rewind(FLEN, (ONE,)) + a.rewind(TLEN, (ONE,)) + a.mark(k+'lex') + a.op('read', FBIN, {'0': k+'f0', ONE: k+'f1', BLANK: k+'equal'}) + a.mark(k+'f0') + a.op('read', TBIN, {'0': k+'same', ONE: k+'done'}) + a.mark(k+'f1') + a.op('read', TBIN, {'0': 'reject', ONE: k+'same'}) + a.mark(k+'same') + a.op('move', FBIN, 1) + a.op('move', TBIN, 1) + a.op('goto', k+'lex') + a.mark(k+'equal') + a.op('read', TBIN, {BLANK: k+'done'}) + a.mark(k+'done') + for tape, symbols in ((FLEN, (ONE,)), (TLEN, (ONE,)), (FBIN, BITS), (TBIN, BITS)): + a.rewind(tape, symbols) + clear(a, tape, symbols) + + +def double(a, tape): + unary_copy(a, tape, DOUBLE, repeat=2) + clear(a, tape) + unary_copy(a, DOUBLE, tape, erase=True) + + +def halve(a, tape): + k = fresh(a, 'halve') + a.mark(k) + a.op('read', tape, {ONE: k+'first', BLANK: k+'done'}) + a.mark(k+'first') + a.op('write', tape, BLANK) + a.op('move', tape, 1) + a.op('read', tape, {ONE: k+'second', BLANK: 'reject'}) + a.mark(k+'second') + a.op('write', tape, BLANK) + a.op('move', tape, 1) + a.op('write', DOUBLE, ONE) + a.op('move', DOUBLE, 1) + a.op('goto', k) + a.mark(k+'done') + a.rewind(tape, (BLANK,)) + a.rewind(DOUBLE, (ONE,)) + unary_copy(a, DOUBLE, tape, erase=True) + + +def product(a, left, right, target): + k = fresh(a, 'product') + a.mark(k+'outer') + a.op('read', left, {ONE: k+'inner', BLANK: k+'done'}) + a.mark(k+'inner') + a.op('read', right, {ONE: k+'bit', BLANK: k+'row'}) + a.mark(k+'bit') + a.op('write', target, ONE) + a.op('move', target, 1) + a.op('move', right, 1) + a.op('goto', k+'inner') + a.mark(k+'row') + a.rewind(right, (ONE,)) + a.op('move', left, 1) + a.op('goto', k+'outer') + a.mark(k+'done') + a.rewind(left, (ONE,)) + a.rewind(target, (ONE,)) + + +def geometry(a): + product(a, S, R, SUFFIX) + unary_copy(a, P, PREFIX) + k = fresh(a, 'geometry') + a.mark(k+'suffix') + a.op('read', F, {ONE: k+'block', BLANK: k+'suffix_done'}) + a.mark(k+'block') + for _ in range(NATIVE_DIMENSION-1): + double(a, SUFFIX) + a.op('move', F, 1) + a.op('goto', k+'suffix') + a.mark(k+'suffix_done') + a.rewind(F, (ONE,)) + a.op('move', F, 1) + a.mark(k+'prefix') + a.op('read', F, {ONE: k+'more', BLANK: k+'done'}) + a.mark(k+'more') + double(a, PREFIX) + a.op('move', F, 1) + a.op('goto', k+'prefix') + a.mark(k+'done') + a.rewind(F, (ONE,)) + for tape in (P, R, S): + clear(a, tape) + + +def copy_width(a, source, target, *, rewind_target=False): + k = fresh(a, 'widthcopy') + a.mark(k) + a.op('read', WIDTH, {ONE: k+'read', BLANK: k+'done'}) + a.mark(k+'read') + a.op('read', source, {str(b): k+str(b) for b in (0, 1)}) + for bit in ('0', ONE): + a.mark(k+bit) + a.op('write', target, bit) + a.op('move', target, 1) + a.op('write', source, BLANK) + a.op('move', source, 1) + a.op('move', WIDTH, 1) + a.op('goto', k) + a.mark(k+'done') + a.rewind(WIDTH, (ONE,)) + if rewind_target: + a.rewind(target, BITS) + + +def load_suffix(a, source, target): + k = fresh(a, 'suffix') + a.mark(k) + a.op('read', SUFFIX, {ONE: k+'pair', BLANK: k+'done'}) + a.mark(k+'pair') + for _ in range(2): + copy_width(a, source, target) + a.op('move', SUFFIX, 1) + a.op('goto', k) + a.mark(k+'done') + a.rewind(SUFFIX, (ONE,)) + a.rewind(target, BITS) + + +def emit_stream(a, source, target): + k = fresh(a, 'stream') + a.mark(k) + a.op('read', source, {str(b): k+str(b) for b in (0, 1)} | {BLANK: k+'done'}) + for bit in ('0', ONE): + a.mark(k+bit) + a.op('write', target, bit) + a.op('move', target, 1) + a.op('write', source, BLANK) + a.op('move', source, 1) + a.op('goto', k) + a.mark(k+'done') + a.rewind(source, (BLANK,)) + + +def tuple_branch(a, label, emit, prefix=()): + """Compile the fixed sixteen branches of a four-symbol read.""" + name = label+''.join(map(str, prefix)) + a.mark(name) + if len(prefix) == 4: + emit(prefix) + else: + a.op('read', INPUTS[len(prefix)], {str(b): name+str(b) for b in (0, 1)}) + for bit in (0, 1): + tuple_branch(a, label, emit, prefix+(bit,)) + + +def c_component(a, signs, output): + """Exact four-input numerator, two sign extensions, halving and fit.""" + k = fresh(a, 'C') + a.mark(k+'seek') + a.op('read', WIDTH, {ONE: k+'seekbit', BLANK: k+'seekend'}) + a.mark(k+'seekbit') + for tape in INPUTS: + a.op('move', tape, 1) + a.op('move', WIDTH, 1) + a.op('goto', k+'seek') + a.mark(k+'seekend') + a.rewind(WIDTH, (ONE,)) + for tape in INPUTS: + a.op('move', tape, -1) + a.op('goto', k+'digit0') + for carry in (-1, 0, 1, 2): + label = k+'digit'+str(carry) + a.mark(label) + a.op('read', WIDTH, {ONE: label+'read', BLANK: k+'extend'+str(carry)}) + def digit(bits, carry=carry): + total = carry+sum(s*b for s, b in zip(signs, bits)) + a.op('write', NUM, str(total % 2)) + a.op('move', NUM, 1) + for tape in INPUTS: + a.op('move', tape, -1) + a.op('move', WIDTH, 1) + a.op('goto', k+'digit'+str(total//2)) + tuple_branch(a, label+'read', digit) + a.mark(k+'extend'+str(carry)) + for tape in INPUTS: + a.op('move', tape, 1) + a.rewind(WIDTH, (ONE,)) + a.op('goto', k+'sign1c'+str(carry)) + for stage in (1, 2): + for carry in (-1, 0, 1, 2): + def extension(bits, carry=carry, stage=stage): + total = carry+sum(s*b for s, b in zip(signs, bits)) + a.op('write', NUM, str(total % 2)) + a.op('move', NUM, 1) + a.op('goto', k+'sign2c'+str(total//2) if stage == 1 else k+'check') + tuple_branch(a, k+'sign'+str(stage)+'c'+str(carry), extension) + a.mark(k+'check') + a.rewind(NUM, BITS) + a.op('read', NUM, {'0': k+'even', ONE: 'reject'}) + a.mark(k+'even') + a.op('write', NUM, BLANK) + a.op('move', NUM, 1) + a.mark(k+'highseek') + a.op('read', NUM, {'0': k+'highstep', ONE: k+'highstep', BLANK: k+'highend'}) + a.mark(k+'highstep') + a.op('move', NUM, 1) + a.op('goto', k+'highseek') + a.mark(k+'highend') + a.op('move', NUM, -1) + a.op('read', NUM, {str(b): k+'top'+str(b) for b in (0, 1)}) + for bit in ('0', ONE): + a.mark(k+'top'+bit) + a.op('write', NUM, BLANK) + a.op('move', NUM, -1) + a.op('read', NUM, {bit: k+'emit'}) + a.mark(k+'emit') + a.op('read', WIDTH, {ONE: k+'emitread', BLANK: k+'done'}) + a.mark(k+'emitread') + a.op('read', NUM, {str(b): k+'emit'+str(b) for b in (0, 1)}) + for bit in ('0', ONE): + a.mark(k+'emit'+bit) + a.op('write', output, bit) + a.op('move', output, 1) + a.op('write', NUM, BLANK) + a.op('move', NUM, -1) + a.op('move', WIDTH, 1) + a.op('goto', k+'emit') + a.mark(k+'done') + a.rewind(WIDTH, (ONE,)) + + +def clone_source(a): + """Clone exactly the generated volume; reject short/excess cardinality.""" + k = fresh(a, 'clone') + a.mark(k+'prefix') + a.op('read', PREFIX, {ONE: k+'blocks', BLANK: k+'done'}) + a.mark(k+'blocks') + for side in range(2): + name = k+'side'+str(side) + a.mark(name) + a.op('read', SUFFIX, {ONE: name+'coefficient', BLANK: name+'done'}) + a.mark(name+'coefficient') + for component in range(2): + field = name+'field'+str(component) + a.mark(field) + a.op('read', WIDTH, {ONE: field+'read', BLANK: field+'done'}) + a.mark(field+'read') + a.op('read', DATA, {str(b): field+str(b) for b in (0, 1)}) + for bit in ('0', ONE): + a.mark(field+bit) + a.op('write', A, bit) + a.op('move', A, 1) + a.op('move', DATA, 1) + a.op('write', DTRACE, ONE) + a.op('move', DTRACE, 1) + a.op('move', WIDTH, 1) + a.op('goto', field) + a.mark(field+'done') + a.rewind(WIDTH, (ONE,)) + a.op('move', SUFFIX, 1) + a.op('goto', name) + a.mark(name+'done') + a.rewind(SUFFIX, (ONE,)) + a.op('move', PREFIX, 1) + a.op('goto', k+'prefix') + a.mark(k+'done') + a.rewind(PREFIX, (ONE,)) + a.op('read', DATA, {BLANK: k+'verified'}) + a.mark(k+'verified') + trace_return(a, DATA, DTRACE) + a.rewind(A, BITS) + + +def commit(a, source): + k = fresh(a, 'commit') + a.mark(k) + a.op('read', source, {str(b): k+str(b) for b in (0, 1)} | {BLANK: k+'done'}) + for bit in ('0', ONE): + a.mark(k+bit) + a.op('write', DATA, bit) + a.op('write', source, BLANK) + a.op('move', source, 1) + a.op('move', DATA, 1) + a.op('write', DTRACE, ONE) + a.op('move', DTRACE, 1) + a.op('goto', k) + a.mark(k+'done') + trace_return(a, DATA, DTRACE) + a.rewind(source, (BLANK,)) + + +def compile_leaf(): + a = Builder() + for tape in PRIVATE: + a.op('move', tape, -1) + a.op('write', tape, MARK) + a.op('move', tape, 1) + gamma(a, F, (FBIN, FLEN)) + for tape in (R, P, S, WIDTH): + gamma(a, tape) + gamma_binary(a) + trace_return(a, HEADER, HTRACE) + cutoff_guard(a) + for i in range(2): + a.op('read', WIDTH, {ONE: 'width'+str(i)}) + a.mark('width'+str(i)) + a.op('move', WIDTH, 1) + a.rewind(WIDTH, (ONE,)) + geometry(a) + clone_source(a) + a.op('write', MODE, '0') + a.mark('prefix') + a.op('read', PREFIX, {ONE: 'load_select', BLANK: 'axis_end'}) + a.mark('load_select') + a.op('read', MODE, {'0': 'loadA', ONE: 'loadB'}) + for mode, source in enumerate((A, B)): + a.mark('load'+('A' if mode == 0 else 'B')) + load_suffix(a, source, LEFT) + load_suffix(a, source, RIGHT) + a.op('goto', 'pairs') + a.mark('pairs') + a.op('read', SUFFIX, {ONE: 'pair', BLANK: 'pairs_done'}) + a.mark('pair') + for source, target in ((LEFT, AR), (LEFT, AI), (RIGHT, BR), (RIGHT, BI)): + copy_width(a, source, target, rewind_target=True) + for signs, output in zip(ROWS, (LOUT, LOUT, ROUT, ROUT)): + c_component(a, signs, output) + for tape in INPUTS: + clear(a, tape, BITS) + a.op('move', SUFFIX, 1) + a.op('goto', 'pairs') + a.mark('pairs_done') + a.rewind(SUFFIX, (ONE,)) + for tape in (LEFT, RIGHT): + a.rewind(tape, (BLANK,)) + for tape in (LOUT, ROUT): + a.rewind(tape, BITS) + a.op('read', MODE, {'0': 'mergeB', ONE: 'mergeA'}) + for name, target in (('mergeB', B), ('mergeA', A)): + a.mark(name) + emit_stream(a, LOUT, target) + emit_stream(a, ROUT, target) + a.op('goto', 'prefix_done') + a.mark('prefix_done') + a.op('move', PREFIX, 1) + a.op('goto', 'prefix') + a.mark('axis_end') + a.op('read', MODE, {'0': 'endA', ONE: 'endB'}) + for mode, source, target in ((0, A, B), (1, B, A)): + name = 'end'+('A' if mode == 0 else 'B') + a.mark(name) + a.op('read', source, {BLANK: name+'valid'}) + a.mark(name+'valid') + a.rewind(source, (BLANK,)) + a.rewind(target, BITS) + a.op('write', MODE, str(1-mode)) + a.op('goto', 'axis_done') + a.mark('axis_done') + a.rewind(PREFIX, (ONE,)) + a.op('move', F, 1) + a.op('read', F, {ONE: 'next_axis', BLANK: 'finish'}) + a.mark('next_axis') + double(a, SUFFIX) + halve(a, PREFIX) + a.op('goto', 'prefix') + a.mark('finish') + a.op('read', MODE, {'0': 'commitA', ONE: 'commitB'}) + for name, source in (('commitA', A), ('commitB', B)): + a.mark(name) + commit(a, source) + a.op('goto', 'retire') + a.mark('retire') + a.rewind(F, (ONE,)) + for tape in (F, WIDTH, PREFIX, SUFFIX): + clear(a, tape) + clear(a, MODE, BITS) + for tape in PRIVATE: + a.op('move', tape, -1) + a.op('write', tape, BLANK) + a.op('move', tape, 1) + a.op('halt') + a.mark('reject') + a.op('read', HEADER, {}) + return a.finish((BLANK, '0', ONE, MARK)) + + + + diff --git a/research/literal-positive-c-leaf/reference/02-streams.tex b/research/literal-positive-c-leaf/reference/02-streams.tex new file mode 100644 index 0000000000..088fceea18 --- /dev/null +++ b/research/literal-positive-c-leaf/reference/02-streams.tex @@ -0,0 +1,208 @@ +\section{The machine model and elementary streams} +\label{sec:streams} + +A machine has one fixed finite alphabet and one fixed finite number of +one-dimensional tapes. A step reads and writes at most one cell on each +tape and moves each head by at most one cell. Fixed tracks and finitely +many work tapes change time by a fixed factor. We distinguish moving one +digit in a fixed radix, which needs a bounded number of scans, from +interchanging fields whose numbers of digits grow. The latter permutation +will be realized in Section~\ref{sec:tape-interchange} by computing XOR +combinations of intermediate data streams. The present section supplies +the elementary scans it uses. Every scan includes its counters and the +return of its tape heads. + +\subsection{Array order and elementary scans} + +For a positive integer $a$ write $[a]=\{0,\ldots,a-1\}$. +An array with address set $[a_1]\times\cdots\times[a_t]$ is stored in +lexicographic order, with the first coordinate most significant. Its +entries are bits unless a record width is specified. A trailing record +of $B$ bits can equivalently be regarded as a final address field $[B]$. +An address is implicit in an entry's position in this ordered stream; it +is not stored beside every data bit. +The \emph{logical volume} $V$ is the number of stored data bits. Work +tapes and duplicate streams are charged in time but do not increase $V$ +in recurrences. All the fields discussed below are nonempty. A call +with an empty array is handled directly. + +An address permutation $f$ moves the entry at $x$ to $f(x)$. Thus its +action on an array $A$ is $(fA)(f(x))=A(x)$. Adjacent fields which are +irrelevant to an operation may be replaced by a single field whose length +is their product. In particular, the elementary procedures below have a +fixed number of formal address fields even when a surrounding algorithm +has a growing list of coordinates. Lengths and positions are supplied in +canonical binary on descriptor tapes; no additional tape head is attached to an +address coordinate. Each elementary call receives a fixed number of +collapsed canonical lengths. Constructing them from a longer surrounding +list is work of the caller; recursive calls below construct their own +collapsed descriptors within their stated bounds. + +When one address field is designated as a row field, collapse the fields +before it to a prefix $[P]$ and those after it to a suffix $[B]$. If the +row field has range $[R]$, a \emph{row} at prefix $p$ and row index $r$ +is the complete consecutive block $\{p\}\times\{r\}\times[B]$. +Every row therefore contains $B$ bits in the same suffix order. + +For headers that concatenate a list of positive integer parameters, we use +the self-delimiting code +\begin{equation} + b_v=\lfloor\log_2v\rfloor+1,\qquad + \Gamma(v)=0^{b_v-1}\operatorname{bin}_{b_v}(v),\qquad + |\Gamma(v)|=2b_v-1\quad(v\ge1). + \label{eq:integer-descriptor-code} +\end{equation} +The initial zeroes specify how many further bits follow the first one, +so concatenated codes can be read in order. We use this code when an +interface specifies a header; elementary calls still receive the fixed +number of canonical binary lengths described above. + +\begin{lemma}[Elementary stream operations] +\label{lem:elementary-streams} +Fix a radix $q\ge2$. Each of the following operations on an array of +volume $V$ takes $O(V)$ steps on a fixed number of one-dimensional tapes: +\begin{enumerate} +\item any fixed permutation of the pair of digit values at two specified +radix-$q$ positions, whether or not the positions are adjacent; +\item moving one specified radix-$q$ digit to another position, preserving +the order of the intervening positions; +\item splitting on a specified radix-$q$ digit, applying a fixed +pointwise map to aligned streams, and merging them back; +\item for positive integers $P,R,B$, within each prefix of an array on +$[P]\times[R]\times[B]$, splitting +whole rows cyclically into a fixed number $W$ of streams, and, when $W$ +divides $R$, merging those streams in any fixed order of the row classes. +\end{enumerate} +The bounds include shape preparation, counter initialization and resets, +and returning or clearing the visited portions of work tapes. Their +constants may depend on the fixed radix, the fixed pointwise map, and the +fixed number of row classes. +\end{lemma} + +\begin{proof} +For the first operation split into $q^2$ streams according to the two +specified digits. With these digits fixed, the order of all remaining +digits is unchanged by the permutation. Enumerate output addresses in +their required order and read the stream prescribed by the two preimage +digits. For a digit move use $q$ streams instead. The same observation +shows that splitting on one digit gives streams with the same remaining +address set in the same order. Scan their aligned entries, apply the +fixed pointwise map, and merge according to the output digit; this proves +the third operation. For the fourth, write $r=Wg+w$, where +$0\le w>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<cutoff` is rejected before payload mutation, rather than executing an +unpriced direct replacement for a recursive child. + +Every address record contains `r>=1` complex coefficients on one fixed common +grid, each component stored in `h>=2` least-significant-first two's-complement +bits followed by virtual delimiter 2. Real precedes imaginary. Current +virtual symbols use three physical bits. Thus + +``` +b = 6 r(h+1), row_bits = 2^a b, +V = C 2^a b, R = 2hr, Vraw = C 2^a R. +``` + +Each successive component has the same width and delimiter; every coefficient +and every spectator address is present. The wrapper verifies `b`, the complete +row extent and all input/return frontiers. It never obtains a payload length +from a host array or a hardware head address. + +For an address `x`, define the current selected positions counted from the +left by `u+jK+rho`, `0<=j=1, including encoded old setup, +complete-axis movement, cleanup, protected return and rejection cleanup. + +Current format import/export and guide restoration cost O(V). The h-bit +component counter has O(h) aggregate initialization/decrement/cleanup cost; +there is no fresh long width scan per payload bit. The first-width scan is +included. Since the canonical `row_bits` binary digits have length at least +a and `b` records the coefficient/width factor, one-time encoded products, +division, comparison and power construction cost at most O((E+1)^4). This +deliberately conservative bound charges large unused metadata too. + +The shared codec refines each old alphabet symbol to four virtual bits and +then twelve current physical positions. Its source-control and local-origin +guards have a fixed overhead factor, not a unit-cost address oracle. The new +leaf cohort needs no parking engine or ordinary object: 216 old engine +scratch roles, its protected output, 128 separate wrapper roles and four +persistent bridge/guide roles give exactly Q=349 ports. The setup live-role +census is fewer than 80, including all 23 header Counts and nested arithmetic +temporaries. Suspended wrapper roles and engine roles are physically distinct. + +A complete physical bill is + +``` +T_current <= F_template + C_codec T_leaf + + C (V + (E+1)^4 + Q) + 64 (Z+Q). +``` + +Every reached old symbol requires movement or initialization within this +call, so `Z=O(T_leaf+V+(E+1)^4+Q)`. Since `Vraw<=V`, this yields + +``` +T_current = F_template + O(fV + (E+1)^4 + Q). +``` + +The last displayed estimate includes copying, source access, formatting, +normalization, cleanup and all numerical leaf work. No faster nonleaf tariff +or empirical speedup is inferred from it. If the actual globally certified +cutoff is `max(N,floor(h^eta))`, then a successful branch has +`f<=N+h^eta` and the corresponding bound is +`F_template+O(V(N+h^eta)+(E+1)^4+Q)`. To compare it with a global selected +tariff one must still supply the actual N, eta, relation of h to the root +precision, the descriptor-growth law and all other caller charges. That +comparison is not asserted here. + +For fresh calls, the source gives each of its finitely many roles backing +`O(Vraw+log(Vraw+1))`; wrapper guides/bridge need O(V) physical storage and +header/setup need a conservative O((E+1)^2). Multiplying old extents by twelve +and retaining fixed Q yields total fresh backing `O_Q(V+(E+1)^2+1)`, in +addition to the protected caller ancestor and public/context storage. +The predecessor's finer occupied-content bound is retained separately from +this conservative fixed-role backing bound. + +Clearing erases contents without shrinking previously visited storage. At a +common fixed origin, the retained backing of role i after completed calls +1..j is at least its historical maximum and is bounded by the maximum of the +displayed per-call envelopes, plus origin/ancestor offsets. More explicitly, +if its old extent on call k is z_i(k) at physical origin o_i(k), charge + +``` +sum_i max_(k<=j) (o_i(k) + 12 z_i(k) + O(1)), +``` + +plus borrowed public/context backing and the caller continuation bank. +The same physical origins may be reused only after the source closure/erase +boundary. A smaller subsequent call encounters fresh physical blanks after +its own current frontier and does not rescan old blank historical backing. + +## 7. Evidence and boundaries + +The full current packets are checked against a separately written direct +Kronecker-coefficient matrix oracle. The oracle sums all `2^f` input values +for each selected-fibre output; it does not call the retained butterfly, +split/merge, carry code or helper alignment routines. It checks all records, +coefficients, signs and output format. Physical fixtures cover spaced offsets, +multiple outer/inner rows, forward/inverse tensors, dirty spectators, named +later-field parity and overflow failures, valid retry and shrinking history. + +Source/token, alias, wrong-offset, wrong-direction and corrupted-source +controls reject. A no-ordinary-constructor control confirms the new direct +leaf does not depend on the older ordinary service. Normal and optimized +replays are regression/coverage evidence. The quantified claim follows from +the preceding source composition argument and its explicit premises, not from +finite sampling or rerunning one implementation. + +The actual source token is exercised on a reduced current descriptor fixture; +it is not an execution of the enormous selected rank-nine complete packet. +No production native exponent, complete selected recurrence, flat-table +export, full source word or integer recovery is tested. All five selected +framework assumptions remain on the selected certificate. This is one +constructed physical leaf boundary, not a new kappa or an unconditional +integer-multiplication theorem. + +## Open next questions + +1. Export this finite source refinement to the actual flat primitive table + syntax and prove its relation to the source control, including the same + rejection boundary. The existing source adapter does not itself fill + `Controller.services` with tables. +2. Compose the actual current monomial entrance, this positive child and its + monomial exit under one source occurrence and precision allocation. Keep + each owner and source order explicit; a matching token is not a completed + MOVE execution. +3. Bind the cutoff and descriptor/word growth laws to the complete current + recurrence. The direct bill is suitable only where the certified cutoff + admits it; no accelerated arbitrary-width substitution follows. diff --git a/research/literal-positive-c-leaf/reference/current-coded-README.md b/research/literal-positive-c-leaf/reference/current-coded-README.md new file mode 100644 index 0000000000..753a44f2b3 --- /dev/null +++ b/research/literal-positive-c-leaf/reference/current-coded-README.md @@ -0,0 +1,67 @@ +# Execute a current coded positive Gaussian leaf + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. **No new κ.** + +This package fills one source-relative numerical boundary of the current +compiled caller: its positive rank-one `PAID` leaf, on complete three-bit-coded +signed complex fields and the actual twenty-three-field runtime descriptor. +The source binder identifies owner 236 and MOVE 9896 of the selected #6030 +word. The surrounding monomial entrance/exit remain separate. + +The provider executes #3091's unchanged physical C kernel and complete encoded +axis traversal. It preserves every coefficient, spectator, delimiter, header +and protected ancestor; named exactness/headroom failures preserve the public +input, erase the private work and allow a valid retry. All work uses **349 +fixed ports**. It constructs and calls **no ordinary supplier**. + +The new result is the current-format/descriptor/source-token join and its +complete physical cost/backing proof. The C identity, fused arithmetic, +tensor-grid reserve and old direct-leaf tariff are credited predecessors. +[PROOF.md](PROOF.md) states the all-size theorem, numerical premises and exact +normalization. It is a source-level finite-control refinement; a literal +`Controller.execute_table` exporter is still needed. + +For physical input V, descriptor length E and positive column count f, the +complete cost is `F_template + O(fV + (E+1)^4 + 349)`. The implementation checks +`f<=cutoff`. It does not substitute this direct bill for the faster recursive +nonleaf service. Historical visited backing remains charged after erasure. + +## Reproduction + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/current-coded-gaussian-leaf +``` + +Expected: `PASS_CURRENT_CODED_GAUSSIAN_LEAF`, `PASS_CURRENT_LEAF_CONTROLS` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. [VERIFY.json](VERIFY.json) registers the +bounded normal/optimized replays. [VERIFICATION.md](VERIFICATION.md) records +what actually ran, the negative controls and the independent review boundary. + +## Sources, novelty and limits + +Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. [SOURCES.json](SOURCES.json) +pins canonical inputs. [DEPENDENCIES.json](DEPENDENCIES.json) authenticates +all copied computational bytes and their origins. The current codec dependency +is published at `CubeJerry/integer-mult-bounds@5629e7772d1720d6727465e328a45694f8620538`; +[BINDING-SOURCE-TREE.json](BINDING-SOURCE-TREE.json) records its independently +retrieved Git tree entries. No uncommitted predecessor is imported. + +Credit Jose Manuel (`jmbarrancoml`) and #3091, the #3087/#3055 tape/monomial +lineage, Alejandro Zarzuelo Urdiales, Nick Petalas, James Chang, AAAmirinu, +DreamingOfClouds' #6030 word, the retained current lifecycle/row dispatcher +authors, and the source-specific notices. See [NOTICE.md](NOTICE.md). + +This is distinct from #6890's caller algebra, #6900/#6901's ideal precision, +the current monomial adapter and current ADD/SCALE work. The complete source +token fixture uses reduced geometry; it is not a selected rank-nine production +packet. A complete caller, admitted global cutoff/stock/precision costs, +nonleaf service, flat table and analytic recovery remain open. All five +foundational assumptions remain on the selected record. + +## Open next questions + +The structured questions and their first useful steps are in [TASK.json](TASK.json) +and the proof: export the actual service table, compose one complete current +MOVE, and integrate the certified direct-leaf cutoff with the full recurrence. diff --git a/research/literal-positive-c-leaf/reference/native_verify.py b/research/literal-positive-c-leaf/reference/native_verify.py new file mode 100644 index 0000000000..2c209dfa9c --- /dev/null +++ b/research/literal-positive-c-leaf/reference/native_verify.py @@ -0,0 +1,277 @@ +"""Check native operators with exact Gaussian dyadic arithmetic. + +The interpreter is adapted from the independent campaign native review. +It does not import the source-code producer or the Clifford compiler. +Research used OpenAI Codex under the user's direction. +""" + +from functools import lru_cache + + +def require(condition, label): + if not condition: + raise ValueError(label) + + +def parity(value): + return value.bit_count() % 2 + + +def mul(matrix, vector): + return sum(parity(row & vector) << i for i, row in enumerate(matrix)) + + +def transpose(matrix): + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(matrix)) for j in range(len(matrix))) + + +def inverse(matrix): + n = len(matrix) + rows = [row | (1 << (n+i)) for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i] >> j & 1), None) + require(pivot is not None, 'singular binary chart') + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(n): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + require([row & ((1 << n)-1) for row in rows] == [1 << i for i in range(n)], 'binary inverse') + return tuple(row >> n for row in rows) + + +def extend(vectors, n): + columns, pivots = [], {} + for value in tuple(vectors) + tuple(1 << i for i in range(n)): + reduced = value + while reduced: + j = reduced.bit_length()-1 + if j not in pivots: + pivots[j] = reduced + columns.append(value) + break + reduced ^= pivots[j] + require(len(columns) == n, 'frame basis extension') + return tuple(columns) + + +def adjoint(circuit): + out = [] + for gate in reversed(circuit): + if gate[0] == 'P': + out.append(('P', inverse(gate[1]))) + elif gate[0] == 'D': + out.append(('D', gate[1], tuple(-a % 4 for a in gate[2]))) + elif gate[0] == 'C': + out.append(('C', gate[1], -gate[2])) + elif gate[0] == 'phase': + out.append(('phase', -gate[1] % 4)) + else: + require(gate[0] == 'X', 'adjoint gate type') + out.append(gate) + return tuple(out) + + +def fourier(rank): + return tuple(('C', 1 << i, 1) for i in range(rank)) + + +def frame(vectors, n): + rank = len(vectors) + if rank == 0: + return () + if rank == n: + return fourier(n) + matrix = transpose(extend(vectors, n)) + columns = transpose(inverse(matrix)) + quadratic = tuple((1 << i) ^ sum(parity(a & b) << j for j, b in enumerate(columns)) for i, a in enumerate(columns)) + diagonal = tuple((row >> i) & 1 for i, row in enumerate(quadratic)) + chart = (('P', matrix), ('D', quadratic, diagonal)) + return adjoint(chart) + fourier(rank) + chart + + +def monomial(record): + matrix = tuple(record['matrix_rows']) + quadratic = tuple(record['quadratic_rows']) + linear = tuple(record['linear_Z4']) + require(transpose(quadratic) == quadratic, 'quadratic symmetry') + require(len(matrix) == len(quadratic) == len(linear) == 9, 'monomial dimension') + require(all(a % 2 == (quadratic[i] >> i) & 1 for i, a in enumerate(linear)), 'diagonal parity') + inverse(matrix) + return (('D', quadratic, linear), ('P', matrix), ('X', record['offset']), ('phase', record['phase'])) + + +def recipe(record): + rank = record['rank'] + require(isinstance(rank, int) and 0 <= rank <= 9, 'child rank') + if rank == 0: + require(record['right'] is None, 'rank zero right factor') + return monomial(record['left']) + return monomial(record['right']) + fourier(rank) + monomial(record['left']) + + +def tableau(circuit, n=9): + rows = [(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)] + for gate in circuit: + tag = gate[0] + out = [] + inverse_transpose = transpose(inverse(gate[1])) if tag == 'P' else None + for x, z, phase in rows: + if tag == 'P': + x, z = mul(gate[1], x), mul(inverse_transpose, z) + elif tag == 'X': + phase += 2 * parity(z & gate[1]) + elif tag == 'C': + if parity(z & gate[1]): + x ^= gate[1] + phase += 3 * gate[2] + elif tag == 'D': + quadratic, linear = gate[1:] + phase += sum(linear[i] for i in range(n) if x >> i & 1) + phase += 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(n) if x >> i & 1) + z ^= mul(quadratic, x) + else: + require(tag == 'phase', 'tableau gate type') + out.append((x, z, phase % 4)) + rows = out + return tuple(rows) + + +@lru_cache(maxsize=512) +def action(gate): + if gate[0] == 'P': + return tuple(mul(gate[1], x) for x in range(512)) + require(gate[0] == 'D', 'state action type') + quadratic, linear = gate[1:] + return tuple((sum(linear[i] for i in range(9) if x >> i & 1) + + 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(9) if x >> i & 1)) % 4 for x in range(512)) + + +def rotate(pair, power): + a, b = pair + return ((a, b), (-b, a), (-a, -b), (b, -a))[power % 4] + + +def state(circuit, basis=0): + value, denominator = {basis: (1, 0)}, 0 + for gate in circuit: + tag = gate[0] + result = {} + if tag == "C": + direction, sign = gate[1:] + for address, (a, b) in value.items(): + for target, pair in ((address, (a - sign*b, b + sign*a)), + (address ^ direction, (a + sign*b, b - sign*a))): + old = result.get(target, (0, 0)) + result[target] = (old[0] + pair[0], old[1] + pair[1]) + denominator += 1 + else: + for address, pair in value.items(): + if tag == "P": + target = mul(gate[1], address) + elif tag == "X": + target = address ^ gate[1] + else: + target = address + if tag == "D": + pair = rotate(pair, action(gate)[address]) + else: + require(tag == "phase", "Unknown Gaussian state gate") + pair = rotate(pair, gate[1]) + require(target not in result, "A monomial address map is not injective") + result[target] = pair + value = {address: pair for address, pair in result.items() if pair != (0, 0)} + while denominator and all((a | b) % 2 == 0 for a, b in value.values()): + denominator -= 1 + value = {address: (a//2, b//2) for address, (a, b) in value.items()} + return value, denominator + + +def equal(actual, expected, label): + require(tableau(actual) == tableau(expected), label + ": signed Pauli action") + require(state(actual) == state(expected), label + ": exact global phase") + + +def verify(data, certificate): + word = data["word"] + original, clean = data["programs"], data["clean_programs"] + source_recipes = data["recipes"] + residuals = data["residuals"]["recipes"] + native_tags = {"climb", "adapter", "residual_adapter"} + for orientation in ("forward", "backward"): + native = [event for event in clean[orientation] if event[0] in native_tags] + require(native == [event for event in original[orientation] if event[0] in native_tags], + "A retained native event changed") + require(len(native) == 5056, "The retained native event count changed") + frames = [frame(tuple(vectors), 9) for vectors in word["frames"]] + used = {(event[3], event[4]) for program in clean.values() + for event in program if event[0] == "climb"} + children = {(record["old"], record["new"]): record for record in source_recipes["children"]} + require(len(children) == len(source_recipes["children"]) and used <= set(children), + "The retained child recipe coverage is incomplete") + for old, new in sorted(used): + record = children[old, new] + require(record["rank"] == len(word["frames"][new]) - len(word["frames"][old]), + "A retained child has the wrong rank") + equal(recipe(record), adjoint(frames[old]) + frames[new], "Retained child") + endpoints = {(record["role"], record["port"]): record + for record in source_recipes["endpoint_adapters"]} + require(len(endpoints) == len(source_recipes["endpoint_adapters"]) + and set(endpoints) == {(role, p) for role in ("source", "target") for p in range(112)}, + "The endpoint adapter coverage is incomplete") + for (role, port), record in endpoints.items(): + direction = word["ports"][port] + conventional = (("C", direction, 1),) if role == "source" else ( + ("C", direction, -1),) + fourier(9) + index = word["start"][port] if role == "source" else word["final"][112 + port] + require(record["frame"] == index and record["rank"] == 0, "An endpoint frame changed") + equal(recipe(record), adjoint(conventional) + frames[index], "Endpoint adapter") + used_residuals = set() + for program in clean.values(): + for event in program: + if event[0] != "residual_adapter": + continue + _, position, register, entry, *tail = event + terminal = tail[0] if tail else 1 + key = str(entry) if terminal == 1 else str(entry) + ":" + str(terminal) + require(key in residuals and position in ("pre", "post"), "A residual binding changed") + require(entry == word["start"][register] and terminal == word["final"][register], + "A residual endpoint changed") + used_residuals.add(key) + for key in sorted(used_residuals): + record = residuals[key] + equal(recipe(record), adjoint(frames[record["frame"]]) + frames[record.get("terminal", 1)], + "Residual adapter") + records = certificate["input_recipes"] + ports = certificate["compensation_ports"] + require([record["port"] for record in records] == ports and len(records) == 8, + "The eight input recipes changed") + columns = 0 + for item in records: + port, label = item["port"], item["label"] + require(label == word["ports"][port] and item["canonical_start_frame_id"] == word["start"][port], + "An input recipe has the wrong supplier label") + record = item["recipe"] + require(record["rank"] == 1, "An input copy has the wrong child rank") + for side in ("left", "right"): + factor = record[side] + require(factor["quadratic_rows"] == [0] * 9 and factor["linear_Z4"] == [0] * 9 + and factor["offset"] == factor["phase"] == 0, + "An input factor is not an address permutation") + actual, expected = recipe(record), (("C", label, 1),) + equal(actual, expected, "Positive inherited input line") + for basis in range(512): + require(state(actual, basis) == state(expected, basis), "A complete input Gaussian column differs") + columns += 1 + negative = monomial(record["right"]) + (("C", 1, -1),) + monomial(record["left"]) + require(tableau(negative) != tableau(expected) or state(negative) != state(expected), + "An inverse input child was not detected") + phased = actual + (("phase", 1),) + require(tableau(phased) == tableau(actual) and state(phased) != state(expected), + "An input phase-only error was not detected") + return {"status": "PASS_EXACT_INPUT_NATIVE_FRAMES", "retained_native_events_per_orientation": 5056, + "retained_child_recipes": len(used), "endpoint_adapter_recipes": len(endpoints), + "residual_adapter_recipes": len(used_residuals), "new_input_recipes": len(records), + "new_exact_gaussian_columns": columns, "inverse_input_child_controls": len(records), + "phase_only_controls": len(records), "address_permutation_factors": 2 * len(records), + "method": "Independent signed Pauli and exact Gaussian interpretation; no compiler import", + "scope": "Positive inherited input frames before every retained adapter. No recursive hosting claim."} diff --git a/research/literal-positive-c-leaf/reference/packed-phase-PROOF.md b/research/literal-positive-c-leaf/reference/packed-phase-PROOF.md new file mode 100644 index 0000000000..46a43bf214 --- /dev/null +++ b/research/literal-positive-c-leaf/reference/packed-phase-PROOF.md @@ -0,0 +1,336 @@ +# A literal quadratic phase for a current selected native recipe + +**Scoped enabling lemma; no new kappa.** Prepared for Jerry Chen / @CubeJerry +with substantial OpenAI assistance. Canonical base: +`e54523517d0f03e58352e647c403a5af3e525a57`. + +## 1. Exact claim, source and novelty + +Fix the nine-coordinate right monomial in the lowering of the actual retained +#7000 native `MOVE` at zero-based program index **24472**: +`["MOVE",415,3,99,false]`. Its before/after frames are 3 and 99 and its +proper-width central child has rank 1. The source is +`research/shared-wire-split-composition/data/final.json.gz`, compressed SHA256 +`2b94953dc14a122e3ef089633f05b58ec689ec5156feb7c784ed3e137dc01883`, +with canonical uncompressed JSON SHA256 +`91429a6b96729292a8764836e00c87a6f7cd3b76f05159033f4867f69a98d097`. +This is a current selected source event, not the historical event8814 fixture. + +`RECIPE.json` retains the whole exact lowering, including both monomial +recipes. The right factor has constant phase 1, linear coefficients +`(3,3,3,3,0,3,3,2,0)`, and symmetric quadratic row masks +`(111,111,111,111,0,111,111,0,0)`. Diagonal entries are already included in +the linear coefficients; only strictly upper matrix entries contribute +quadratic terms. With `J={0,1,2,3,5,6}`, its input-coordinate phase is + +\[ +q(x)=1+3\sum_{i\in J}x_i+2x_7+ + 2\sum_{i