From b8dd4e04bf8490aca121abc7ba0e503651db6c97 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Mon, 19 Oct 2026 01:19:48 -0700 Subject: [PATCH] Audit every actual P104 tensor-code scalar event and global block identity Retain frozen PR3979 builders and credit. Certify all104-port fibers, exact full-coordinate tensor composition and complete original invoices. No native caller or frontier change. --- .../p104-tensor-word-audit/CERTIFICATE.json | 10 + research/p104-tensor-word-audit/PROOF.md | 186 ++++++++++++ research/p104-tensor-word-audit/README.md | 102 +++++++ research/p104-tensor-word-audit/SOURCES.json | 54 ++++ research/p104-tensor-word-audit/TASK.json | 111 ++++++++ research/p104-tensor-word-audit/VERIFY.json | 38 +++ .../p104-tensor-word-audit/independent.py | 264 ++++++++++++++++++ .../p104-tensor-word-audit/source/PROOF.md | 201 +++++++++++++ .../p104-tensor-word-audit/source/README.md | 78 ++++++ .../p104-tensor-word-audit/source/verify.py | 201 +++++++++++++ .../p104-tensor-word-audit/test_verify.py | 210 ++++++++++++++ research/p104-tensor-word-audit/verify.py | 202 ++++++++++++++ 12 files changed, 1657 insertions(+) create mode 100644 research/p104-tensor-word-audit/CERTIFICATE.json create mode 100644 research/p104-tensor-word-audit/PROOF.md create mode 100644 research/p104-tensor-word-audit/README.md create mode 100644 research/p104-tensor-word-audit/SOURCES.json create mode 100644 research/p104-tensor-word-audit/TASK.json create mode 100644 research/p104-tensor-word-audit/VERIFY.json create mode 100644 research/p104-tensor-word-audit/independent.py create mode 100644 research/p104-tensor-word-audit/source/PROOF.md create mode 100644 research/p104-tensor-word-audit/source/README.md create mode 100644 research/p104-tensor-word-audit/source/verify.py create mode 100644 research/p104-tensor-word-audit/test_verify.py create mode 100644 research/p104-tensor-word-audit/verify.py diff --git a/research/p104-tensor-word-audit/CERTIFICATE.json b/research/p104-tensor-word-audit/CERTIFICATE.json new file mode 100644 index 0000000000..45d263cb27 --- /dev/null +++ b/research/p104-tensor-word-audit/CERTIFICATE.json @@ -0,0 +1,10 @@ +{ + "schema_version": 1, + "ports": 104, + "pivot_ports": 8, + "invoices": { + "boundary": {"add": 319488, "half": 43264, "double": 43264}, + "coded_pair": {"add": 26240, "half": 3328, "double": 3328}, + "reference_pair": {"add": 241280, "half": 41600, "double": 41600} + } +} diff --git a/research/p104-tensor-word-audit/PROOF.md b/research/p104-tensor-word-audit/PROOF.md new file mode 100644 index 0000000000..fe449557f9 --- /dev/null +++ b/research/p104-tensor-word-audit/PROOF.md @@ -0,0 +1,186 @@ +# Source-bound audit of the actual P104 tensor words + +## Scope, sources and operator order + +Chris R / Clear1nsight's PR3979, scientific head +`a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61`, supplies the construction, words, +counts and comparison audited here. Canonical main is +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The new result is a compositional +exact check at the actual 104 ports and all 21,632 data coordinates. It is not +a new code, a criticism of the predecessor's written derivation, or a full +multiplication/native audit. The unchanged exported sources retain their +authorship and earlier P104/native/caller credit. + +All arithmetic below is coordinatewise over the Gaussian dyadic ring +`R=Z[i,1/2]`, under the predecessor's common-FULL-chart scalar contract. +Temporarily modified donors must return. No physical chart transport or owner +reassignment is inferred. Number data by +`index(bank,i,j)=(bank*104+i)*104+j`. The first eight axis coordinates are the +original pivot ports `(0,1,3,6,22,31,93,103)`; the remaining ports retain +canonical lexicographic order. Operators act on column vectors, the rightmost +operator executes first, and `K_r=K tensor I`, `K_c=I tensor K`. Axis zero +varies i at fixed j; axis one varies j at fixed i. + +The canonical P104 fixture is authenticated by SHA256 +`516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4`. +The primary checker obtains the frozen source's actual words and B2=2B; the +independent checker reconstructs roots from a different full ternary/sign +enumeration and never imports a primary or predecessor executable. Both bind +all 768 B2 entries to SHA256 +`88e9a726e8c8aec055bfd7cd024883b5c8ecbda0cd6471e591a08c43a108a535`, +using ASCII `json.dumps(b2,separators=(',',':'))` without a newline. This is the +explicit bridge between literal-word checking and the independently rebuilt +geometry, rather than agreement only on dimensions or support counts. + +## Every literal event has an exact local meaning + +The authenticated source builders generate four complete words: encoder, +decoder, coded Gram pair and specified uncoded reference Gram pair. No +predecessor evaluator, result routine or receipt supplies their semantics. +For every event the primary checker verifies opcode, arity, integer indices +and signed-unit ADD coefficient. Its localization checks that both donors and +recipients lie in the declared bank/fiber. Every word is consumed to its end; +truncation, extra events and a move to another fiber cannot be ignored. + +On the 104 independent local coordinates, an exact sparse Fraction interpreter +certifies the four sweep maps `U,U^-1,U^t,U^-t`. On 208 independent two-bank +local coordinates it certifies the lower/upper M shears and lower/upper A +shears, including complete source return. These are eight distinct local maps. +Every other fiber's full localized event sequence is checked equal to its +certified pattern. Within a fixed sweep, different fibers have disjoint +supports, so these local maps compose to their stated global tensor factors. + +The coverage is 416 encoder fibers, 416 decoder fibers, 16 coded-pair fibers +and 208 reference-pair fibers: **1,056 actual fiber instances**. The four +words together contain **763,392 literal events**, all checked. This is the +sum of one copy of each of the four audited words, not the length of a single +two-pair experiment. Pattern reuse avoids redoing identical arithmetic; it +does not replace inspection of any event or restrict input values. + +Each event index is below `2*104^2`. Therefore the words extend by logical +identity on every additional independently arbitrary helper coordinate, +including the named 72-per-fiber auxiliary banks. This is stronger than +checking only zero dirt or two sentinels, but is solely a logical index fact. +It does not execute their physical completion, native return or ownership. + +## Global algebra on all coordinates + +Let P select the first eight coordinates. The independent reconstruction +checks the actual Gram matrix A, all B entries, and + +``` +U = [I B;0 I], U^-1 = [I -B;0 I], +A = U^t P U, M = U U^t, N = M^-1 = U^-t U^-1. +``` + +The encoder sweeps execute `U_c^-t` before `U_r` on X and `U_c` before +`U_r^-t` on Y. Thus their global map and the certified decoder are + +``` +L = U_r U_c^-t, +C = diag(L,L^-t), C^-1 = diag(L^-1,L^t). +``` + +There is no cross-bank slot permutation. The uncoded lower stage and subsequent +upper stage are + +``` +S = [I 0; A_r I], R = [I -A_c;0 I]. +``` + +Their chronological pair is RS. The two-bank coded fibers implement + +``` +S_hat = C S C^-1 = [I 0; P_r M_c I], +R_hat = C R C^-1 = [I -M_r P_c;0 I]. +``` + +For example, the lower coefficient factors as +`(U^-t A U^-1) tensor (U U^t)=P tensor M`. The upper coefficient is +`M tensor P`. These factors retain the displayed order; replacing M by +`U^t U` is generally incorrect. The independent checker proves both C +inverse identities, both Gram conjugations, and the full endpoints + +``` +C^-1 (R_hat S_hat) C = RS, +C^-1 (R_hat S_hat)^2 C = (RS)^2. +``` + +The same C is used on both sides of the internal boundary. These equalities +hold on every independent real/imaginary component of both banks, including +the Gram kernel. They are not tests of a sampled dense input. + +### Exact contraction without a huge dense matrix + +Each bank-to-bank block is stored as a finite sum `T=sum_k c_k A_k tensor B_k` +of real dyadic 104-by-104 factors. Matrix products preserve this form. Its +exact Frobenius square is + +``` +||T||_F^2 = sum_(k,l) c_k c_l + _F _F. +``` + +This follows by expanding each entry and separating the two tensor indices. +All factor entries are integers divided by powers of two; the implementation +performs integer multiplication and common-denominator addition. There is no +floating point, tolerance or probabilistic contraction. Since T is real, +this sum is zero exactly when every entry of T is zero. Checking all four +two-bank residual blocks therefore proves equality on all **21,632 data +coordinates**, while avoiding their 467,943,424-entry dense operator. +The independent checker verifies eight global block identities in this way. +Its zero contractions combine with the literal-fiber audit above; neither +checker alone is claimed to certify the entire evidence chain. + +## Counts, comparison and the omitted identity requirement + +Counting every generated event gives the predecessor's invoices: + +| Word | Unit ADD/SUB | Halves | Doubles | +| --- | ---: | ---: | ---: | +| Entry plus exit | 319488 | 43264 | 43264 | +| Coded uncorrected Gram pair | 26240 | 3328 | 3328 | +| Specified uncoded Gram pair | 241280 | 41600 | 41600 | + +For k repeated identical **uncorrected Gram pairs**, the charged addition +comparison is `319488+26240k` against `241280k`; each scaling category is +`43264+3328k` against `41600k`. At k=1 the code loses 104448 additions and +4992 operations in each scaling category. At k=2 it saves 110592 additions +and 33280 in each scaling category. Since the respective inequalities are +`215040k>319488` and `38272k>43264`, two is the first positive integer winning +all three columns. This compares precisely these existing words, not optimal +uncoded algorithms, runtime, or an identified physical repeated consumer. + +The required identity shears are different. Their coded coefficients are +`N_r M_c` and `M_r N_c`; the Gram words contain only `P_r M_c` and `M_r P_c`. +The independent checker verifies the identity conjugations and + +``` +N-P = U^-t (I-A) U^-1, A^2=13A. +``` + +Over Q, `(I-A)^-1=I-A/12`. Hence N-P has rank 104 and, since M is invertible, +each omitted tensor side has rank **10816**. This is an algebraic-rank fact, +not a dyadic primitive, native-child tariff or cost lower bound. A nonzero +kernel payload `(-Bz,z)` is retained by U even though its pivot query vanishes; +the omitted identity side acts nontrivially on it. The original PR already +owns these completion warnings and rank claims. + +Positive exact residual norms additionally separate reversed U/transpose +order, reversed Gram-stage order and omitted lower/upper identity completion. +The original modulo-13 spectral-normalization result is outside this audit. + +## Remaining obligations and stopping rule + +This closes a bounded all-coordinate software/algebra audit of the pinned +scalar words. Physical chart conjugation, actual adjacent/repeated consumers, +identity-side implementation, copied-center endpoint correction/wrappers, +dirty-helper completion, owners/routing/holding/control/tapes, signed-floor +precision and all-size/native admission remain unresolved or inherited. Scalar +ADD/scale counts are not native rank units. No new physical bill, passing +supplier inequality, kappa change, human acceptance or proof-kernel certificate +is claimed. Stop dependent construction until a named consumer and favorable +complete allowance are supplied. + +Prepared by ToikY with substantial OpenAI Codex assistance, including separate +AI implementation/review contexts. Apache-2.0; all predecessor credit is retained. diff --git a/research/p104-tensor-word-audit/README.md b/research/p104-tensor-word-audit/README.md new file mode 100644 index 0000000000..4cbb44956a --- /dev/null +++ b/research/p104-tensor-word-audit/README.md @@ -0,0 +1,102 @@ +# P104 tensor-code literal-word audit + +This independently checks the actual scalar programs in [Chris R / Clear1nsight's +PR3979](https://github.com/CrocSwap/integer-mult-bounds/pull/3979) at frozen head +`a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61`. Every one of **763,392 literal +operations** is covered by **1,056 fiber instances, disjoint within each sweep**, reduced to eight +exact local linear maps. A separately implemented exact tensor calculation checks +eight global identities, comprising 32 bank blocks, on all **21,632 data +coordinates**. No coordinate sampling or floating tolerance is used. + +The contribution is source-bound implementation coverage. The tensor code, +algebraic conjugation and protocol savings belong to PR3979. Its written proof +already addresses arbitrary inputs; this audit adds exhaustive actual-instance +word coverage beyond its small-grid basis tests and actual dense fixtures. It +does not supply a new code, physical repeated caller, admitted supplier or κ. + +## Evidence and reproduction + +From the repository root, with Python 3.12 and no third-party requirements: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-tensor-word-audit +``` + +The three registered commands are `verify.py`, `independent.py` and +`test_verify.py`. Direct replay also works from a Git-free committed package +export containing the declared canonical P104 fixture. A package-directory copy +alone omits that external input. `SOURCES.json` pins its exact bytes and the +three package-local predecessor exports; neither an unmerged predecessor commit +nor network access is needed for replay. + +`verify.py` authenticates the frozen constructor before calling its word builders +and geometry constructor. Those builders are the object under review. It never +calls the predecessor evaluator, invoice or result routine. The checker consumes +every event, validates its global data index, bank, axis, sign and chronology, +and evaluates one full basis map for each distinct 104- or 208-coordinate fiber. +Every other fiber is checked for exact program equality after its own physical +index localization; a cached pattern cannot hide an altered later fiber. + +`independent.py` imports neither primary nor predecessor code. It reconstructs +the roots and all 768 signed-half coefficients by a different enumeration. Both +checkers bind this complete ordered coefficient array to the same canonical +digest. It proves the global block identities by exact factored Kronecker +products and Frobenius-square contractions; zero means every matrix entry is +zero. Four deliberately wrong global expressions have strictly positive norms. +See [PROOF.md](PROOF.md) for the composition argument and conventions. + +`test_verify.py` runs 12 semantic word mutations and seven actual CLI damaged +source/invoice cases under both normal and optimized Python: 38 rejections, +plus four separate independent-checker fixture rejections. It also replays the +actual 104-port primary checker normally and optimized from an inode-disjoint, +read-only Git-free closure and verifies unchanged source bytes. These are +software checks and a scoped exact algebra certificate; no human or proof-kernel +review is implied. + +## Recomputed original invoice + +| Named word | Unit ADD | Half | Restoring double | +| --- | ---: | ---: | ---: | +| Encoder plus decoder | 319,488 | 43,264 | 43,264 | +| One coded Gram pair | 26,240 | 3,328 | 3,328 | +| One specified reference Gram pair | 241,280 | 41,600 | 41,600 | + +The claimed two-pair saving is confirmed: 110,592 ADDs and 33,280 halves and +doubles each, with entry and exit paid. One pair loses 104,448 ADDs. These +are PR3979's results against its specified reference, with no optimality claim. +The correct identity-shear coefficients remain `N tensor M` and `M tensor N`, +where `M=UU^t`, `N=M^-1`; the omitted side maps each have rational rank 10,816. +Algebraic rank does not price native calls. Helpers are untouched by the literal +data indices, which proves logical identity extension only. + +## Open next questions + +1. **Actual repeated consumer and shared charts.** Pin one chronological physical + producer/consumer pair and write every data/helper owner and ordered chart + conjugate. This determines whether a shared code can be used at all. No such + physical pair is constructed here; scalar conjugacy does not discharge it. +2. **Complete paid identity caller.** After that interface is fixed, compile the + required `N-P` side maps and code boundaries and price every native transport, + helper, routing and finite-width precision charge. First test the complete + favorable family gate; the isolated repeated-Gram saving cannot justify + construction expansion. All-size and multiplication-theorem admission remain + separate obligations. + +## Attribution and scope + +Chris R / Clear1nsight owns PR3979's tensor construction, scalar word builders, +original proof, invoice and side-map analysis. Its source files are retained +byte-for-byte in `source/`. PR3961 supplies the preceding representation mismatch; +PR3882/3940/3943/3954 retain the caller lineage. ToikY's PR3956 adapter comparison +and PR3966 phase gauge are context, not dependencies of this certificate. +The retained source credits Rohan Arun/PR1972, Chafik Boukhalfa/PR1991, Adam +Gall/PR1940, Josie Elliston and the E8 predecessors, Sagar Thakrar/PR1012, +Douglas Colkitt, Dominik Scholz and the native/compiler/coverage/terminal-floor +contributors named in the preserved source. Their claims outside this scope +were not replayed here. + +New audit, packaging and tests: ToikY with substantial OpenAI Codex assistance, +including separate AI math and test contexts. Apache-2.0. Only this scoped package +is added; canonical main, frozen predecessors and the selected frontier are +unchanged. `TASK.json` records handoff-first selection, overlap coverage and the +change from the catalogue card's original chronological-correction question. diff --git a/research/p104-tensor-word-audit/SOURCES.json b/research/p104-tensor-word-audit/SOURCES.json new file mode 100644 index 0000000000..9d6911c70c --- /dev/null +++ b/research/p104-tensor-word-audit/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ], + "source_exports": [ + { + "path": "research/p104-tensor-word-audit/source/README.md", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61", + "origin_path": "research/p104-tensor-code/README.md", + "git_blob": "be374d54df5d481bdf8d83671c0a3843149dec11", + "sha256": "7c57cda30963c1fc37a96b92182912b3942e4e2447ba599db9f7af2359414d9c", + "usage": "package-local exact source export; primary hardcoded hash authentication; word/geometry builders only are objects under review" + }, + { + "path": "research/p104-tensor-word-audit/source/PROOF.md", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61", + "origin_path": "research/p104-tensor-code/PROOF.md", + "git_blob": "b570c8bdf5acec263c63562ddb5e384ff3616c3f", + "sha256": "259ba7b0926dd6db4e7c45ff7ccb10659dee06aef0a573547236c994ad304756", + "usage": "package-local exact source export; primary hardcoded hash authentication; word/geometry builders only are objects under review" + }, + { + "path": "research/p104-tensor-word-audit/source/verify.py", + "origin_repository": "Clear1nsight/integer-mult-bounds", + "origin_commit": "a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61", + "origin_path": "research/p104-tensor-code/verify.py", + "git_blob": "7b8194642450100fafefde2e3bbb6d4a3daa7194", + "sha256": "27bae82fe247fe49b8fc3b5efbd429e2c8c0ee8f56cc4ace748cbb681a5abacc", + "usage": "package-local exact source export; primary hardcoded hash authentication; word/geometry builders only are objects under review" + } + ], + "source_export_contract": "The pending foreign commit is not a Git-history dependency. All three exact exports are retained in this package and authenticated by the primary checker before import. Its evaluator, invoice and result routines are never called. Independent checker imports no primary/predecessor code and separately reconstructs the canonical live fixture; both bind the complete ordered B2 array. Generic history checks cover canonical files, not foreign origin availability or scientific acceptance." +} diff --git a/research/p104-tensor-word-audit/TASK.json b/research/p104-tensor-word-audit/TASK.json new file mode 100644 index 0000000000..d5a56fa3ec --- /dev/null +++ b/research/p104-tensor-word-audit/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Source-bound exhaustive compositional audit of the actual104-port literal encoder, decoder, coded pair and reference pair in PR3979, with separate all-coordinate factored tensor identities and exact invoice checks.", + "scope_change_reason": "Handoff-first inspection found a useful independent verification obligation in new PR3979. This adds every-operation actual-instance coverage beyond its finite test fixtures without claiming a defect in the written arbitrary-input proof. It does not construct the original card chronological correction or expand native construction.", + "bottleneck_link": "Distinguishes a correctly implemented shared scalar representation from the still-missing repeated physical caller, identity completion and full favorable bill.", + "budget_minutes": 60, + "stop_rule": "Audit only the frozen four scalar words and their stated tensor identities. Stop at exact agreement or a localized counterexample; do not expand native construction. Science stops08:43:59UTC and final15minutes are reserved for verification and handoff.", + "outcome": "partial", + "evidence": "PROOF.md supplies the disjoint-fiber composition and exact zero-norm argument. verify.py consumes763392literal operations across1056fibers/eightlocalmaps; independent.py checks32globalblocks without primary/predecessor imports; test_verify.py supplies38primary/API and4independent negative runs plus read-only actual-instance replay.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, testing and separate AI math/test review contexts; not independent human or proof-assistant review.", + "selection": { + "method": "latest-handoff-first; named catalogue card retained for provenance, no random reroll", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19034741", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/3979#issuecomment-6262687074", + "scope_key": "72dfbf0708467ad34793", + "entry_open_pr_bodies_including_drafts": 684, + "checkpoint": { + "checked_at_utc": "2026-10-19T08:16:10Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "open_pr_bodies_including_drafts": 694, + "pagination": "seven nonempty pages plus empty eighth; no duplicate IDs", + "relevant_head_3979": "a8a1d744811cd7d1f9c43ec7ccbae85ef9695b61", + "decision": "Continue frozen independent audit. PR3981 changes cleanup and PR3984 translated native progress; neither supplies this literal-word coverage. PR3989 occupies the selected rank-two successor and R437 follow-ups are separately claimed. No frontier or priority change." + }, + "coverage_limit": "All open PR bodies including drafts and cached repository helper; live #1166 and relevant current PR comments read. Broader Discussions, closed diffs, unmentioned work and historical source claims remain partially covered. No no-match novelty inference." + }, + "open_questions": [ + { + "question": "Can an actual repeated physical producer and consumer retain the shared tensor code with all data/helper owners and ordered charts?", + "why_it_matters": "All-coordinate scalar implementation agreement does not construct the missing caller.", + "first_step": "Pin one chronological physical pair and specify every entrance, intermediate and exit owner/chart.", + "blocked_by": "No such pair or native shared code is admitted in this audit." + }, + { + "question": "Does a full identity caller with code boundaries, N-P side maps and all native/helper/routing/precision charges clear the family budget gate?", + "why_it_matters": "The credited two-pair Gram saving is only a named scalar protocol comparison.", + "first_step": "After fixing the actual interface, compile and price the complete favorable caller before any construction expansion.", + "blocked_by": "Identity completion, native tariffs and physical finite-width/all-size transfer remain open." + } + ] +} diff --git a/research/p104-tensor-word-audit/VERIFY.json b/research/p104-tensor-word-audit/VERIFY.json new file mode 100644 index 0000000000..13277f507b --- /dev/null +++ b/research/p104-tensor-word-audit/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticate retained builders/live fixture and all768ordered B2 coefficients; consume every763392literal event over1056fibers/eightexactmaps; typed complete invoice." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Independent actual geometry and exact Frobenius contractions of32globalblocks on21632coordinates; four wrong-expression controls; full-rank identity sides scoped algebra only." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "12literal mutations and7damaged actual CLI cases normal/optimized:38primary/API and4independent source rejections; positive full actual104 read-only Git-free closure and unchanged source bytes." + } + ] +} diff --git a/research/p104-tensor-word-audit/independent.py b/research/p104-tensor-word-audit/independent.py new file mode 100644 index 0000000000..98e7a0195e --- /dev/null +++ b/research/p104-tensor-word-audit/independent.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""Exact factored-tensor audit at all actual P104 coordinates. + +Imports no primary or predecessor executable. Literal-event certification is +the companion checker's obligation; this file proves the global block algebra. +Apache-2.0. ToikY with substantial OpenAI Codex assistance. +""" +from __future__ import annotations + +from dataclasses import dataclass +from functools import lru_cache +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FIXTURE_SHA256 = "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" +B2_SHA256 = "88e9a726e8c8aec055bfd7cd024883b5c8ecbda0cd6471e591a08c43a108a535" +PIVOTS = (0, 1, 3, 6, 22, 31, 93, 103) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Dyadic: + rows: tuple + exponent: int = 0 + + +def matrix(rows, exponent=0): + rows = tuple(tuple(row) for row in rows) + require(len(rows) == 104 and all(len(row) == 104 for row in rows), "actual matrix dimension") + require(type(exponent) is int and exponent >= 0 + and all(type(value) is int for row in rows for value in row), "integer dyadic data") + if not any(any(row) for row in rows): + exponent = 0 + else: + while exponent and all(value % 2 == 0 for row in rows for value in row): + rows = tuple(tuple(value // 2 for value in row) for row in rows) + exponent -= 1 + return Dyadic(rows, exponent) + + +def transpose(value): + return matrix(zip(*value.rows), value.exponent) + + +@lru_cache(maxsize=None) +def sparse_rows(value): + return tuple(tuple((index, entry) for index, entry in enumerate(row) if entry) + for row in value.rows) + + +@lru_cache(maxsize=None) +def times(left, right): + result = [] + right_rows = sparse_rows(right) + for row in sparse_rows(left): + output = [0]*104 + for middle, value in row: + for column, coefficient in right_rows[middle]: + output[column] += value*coefficient + result.append(output) + return matrix(result, left.exponent+right.exponent) + + +def linear_combination(left, right, coefficient=1): + exponent = max(left.exponent, right.exponent) + a, b = 1 << (exponent-left.exponent), coefficient << (exponent-right.exponent) + return matrix([[a*x+b*y for x, y in zip(row, other)] + for row, other in zip(left.rows, right.rows)], exponent) + + +@lru_cache(maxsize=None) +def frobenius(left, right): + """Trace(left^t right), as an integer numerator and power-of-two denominator.""" + numerator = sum(x*y for row, other in zip(left.rows, right.rows) for x, y in zip(row, other)) + return numerator, left.exponent+right.exponent + + +def add_dyad(left, right): + exponent = max(left[1], right[1]) + return ((left[0] << (exponent-left[1])) + (right[0] << (exponent-right[1])), exponent) + + +def norm_squared(terms): + """Exact norm of sum sign*A tensor B, without a 10816-square matrix.""" + answer = (0, 0) + for sign, row_factor, column_factor in terms: + for other_sign, other_row, other_column in terms: + left = frobenius(row_factor, other_row) + right = frobenius(column_factor, other_column) + answer = add_dyad(answer, (sign*other_sign*left[0]*right[0], left[1]+right[1])) + require(answer[0] >= 0, "nonnegative exact Frobenius square") + return answer + + +def tensor_product(left, right): + return [(1, left, right)] + + +def tensor_times(left, right): + return [(a*b, times(row, other_row), times(column, other_column)) + for a, row, column in left for b, other_row, other_column in right] + + +def tensor_minus(left, right): + return left + [(-sign, row, column) for sign, row, column in right] + + +def zero_tensor(terms, message): + require(norm_squared(terms)[0] == 0, message) + + +def block_times(left, right): + return [[sum((tensor_times(left[i][k], right[k][j]) for k in range(2)), []) + for j in range(2)] for i in range(2)] + + +def zero_blocks(left, right, message): + for i in range(2): + for j in range(2): + zero_tensor(tensor_minus(left[i][j], right[i][j]), message+" block="+str((i, j))) + + +def nonzero_blocks(left, right, message): + total = (0, 0) + for i in range(2): + for j in range(2): + total = add_dyad(total, norm_squared(tensor_minus(left[i][j], right[i][j]))) + require(total[0] > 0, message) + return {"numerator": total[0], "denominator_power_two": total[1]} + + +def geometry(): + path = ROOT / "research/p104-native-channel/inputs/P104-FIXTURE.json" + raw = path.read_bytes() + require(hashlib.sha256(raw).hexdigest() == FIXTURE_SHA256, "canonical fixture authentication") + fixture = json.loads(raw)["section4_explicit_P104"] + # Enumeration differs from the predecessor's pairs-plus-seven-sign loop. + roots = set() + for row in itertools.product((-2, 0, 2), repeat=8): + support = [value for value in row if value] + if len(support) == 2 and support[0] > 0: + roots.add(row) + for row in itertools.product((-1, 1), repeat=8): + if row[0] == 1 and row.count(-1) % 2 == 0: + roots.add(row) + removed = {tuple(row) for row in fixture["F0"]+fixture["C"]} + require(len(roots) == 120 and len(removed) == 16 and removed <= roots, "independent root domain") + original = sorted(roots-removed) + order = list(PIVOTS)+[i for i in range(104) if i not in PIVOTS] + ports = [original[i] for i in order] + gram = [[sum(x*y for x, y in zip(row, other)) for other in ports] for row in ports] + require(all(gram[i][j] == 8*int(i == j) for i in range(8) for j in range(8)), "orthogonal pivots") + require(all(gram[i][j] % 4 == 0 for i in range(8) for j in range(8, 104)), "half coefficient domain") + b2 = [[gram[i][j]//4 for j in range(8, 104)] for i in range(8)] + require(hashlib.sha256(json.dumps(b2, separators=(",", ":")).encode("ascii")).hexdigest() + == B2_SHA256, "all 768 actual B2 entries") + require(sum(value != 0 for row in b2 for value in row) == 384 + and all(value in (-1, 0, 1) for row in b2 for value in row), "actual B support/alphabet") + require(all(sum(b2[i][k]*b2[j][k] for k in range(96)) == 48*int(i == j) + for i in range(8) for j in range(8)), "actual BBt") + identity = matrix([[int(i == j) for j in range(104)] for i in range(104)]) + pivot = matrix([[int(i == j and i < 8) for j in range(104)] for i in range(104)]) + upper_rows = [[2*int(i == j) for j in range(104)] for i in range(104)] + inverse_rows = [row[:] for row in upper_rows] + for i in range(8): + upper_rows[i][8:] = b2[i][:] + inverse_rows[i][8:] = [-value for value in b2[i]] + upper, inverse = matrix(upper_rows, 1), matrix(inverse_rows, 1) + actual_gram = matrix(gram, 3) + return identity, pivot, upper, inverse, actual_gram, b2 + + +def apply_numerator(value, vector): + return [sum(coefficient*entry for coefficient, entry in zip(row, vector)) for row in value.rows] + + +def audit(): + identity, pivot, upper, inverse, gram, b2 = geometry() + upper_t, inverse_t = transpose(upper), transpose(inverse) + require(times(upper, inverse) == times(inverse, upper) == identity, "U two-sided inverse") + require(times(times(upper_t, pivot), upper) == gram, "actual Gram congruence") + moment = times(upper, upper_t) + moment_inverse = times(inverse_t, inverse) + require(times(moment, moment_inverse) == times(moment_inverse, moment) == identity, "M/N inverse") + require(times(gram, gram) == matrix([[13*x for x in row] for row in gram.rows], gram.exponent), + "A square equals 13A") + require(times(times(inverse_t, gram), inverse) == pivot, "lower one-axis conjugation") + + unit = tensor_product(identity, identity) + lower = [[unit, []], [tensor_product(gram, identity), unit]] + upper_stage = [[unit, [(-1, identity, gram)]], [[], unit]] + coded_lower = [[unit, []], [tensor_product(pivot, moment), unit]] + coded_upper = [[unit, [(-1, moment, pivot)]], [[], unit]] + # C=diag(U tensor U^-t, U^-t tensor U), with its explicit two-sided inverse. + coding = [[tensor_product(upper, inverse_t), []], [[], tensor_product(inverse_t, upper)]] + decoding = [[tensor_product(inverse, upper_t), []], [[], tensor_product(upper_t, inverse)]] + block_identity = [[unit, []], [[], unit]] + zero_blocks(block_times(decoding, coding), block_identity, "global decode/encode identity") + zero_blocks(block_times(coding, decoding), block_identity, "global encode/decode identity") + zero_blocks(block_times(block_times(coding, lower), decoding), coded_lower, "coded lower Gram stage") + zero_blocks(block_times(block_times(coding, upper_stage), decoding), coded_upper, "coded upper Gram stage") + + reference_pair = block_times(upper_stage, lower) + coded_pair = block_times(coded_upper, coded_lower) + zero_blocks(block_times(block_times(decoding, coded_pair), coding), reference_pair, "decoded one-pair endpoint") + reference_twice = block_times(reference_pair, reference_pair) + coded_twice = block_times(coded_pair, coded_pair) + zero_blocks(block_times(block_times(decoding, coded_twice), coding), reference_twice, + "decoded two-pair all-coordinate endpoint") + + # Corrected identity shears have different, full-dimensional coefficients. + plain_identity_lower = [[unit, []], [unit, unit]] + plain_identity_upper = [[unit, [(-1, identity, identity)]], [[], unit]] + completed_lower = [[unit, []], [tensor_product(moment_inverse, moment), unit]] + completed_upper = [[unit, [(-1, moment, moment_inverse)]], [[], unit]] + zero_blocks(block_times(block_times(coding, plain_identity_lower), decoding), completed_lower, + "corrected identity lower coefficient") + zero_blocks(block_times(block_times(coding, plain_identity_upper), decoding), completed_upper, + "corrected identity upper coefficient") + side = linear_combination(moment_inverse, pivot, -1) + expected_side = times(times(inverse_t, linear_combination(identity, gram, -1)), inverse) + require(side == expected_side, "identity completion side congruence") + # (I-A)(I-A/12)=I follows from A^2=13A. The inverse is used over Q only; + # this is an algebraic full-rank argument, not a dyadic primitive or tariff. + square = times(gram, gram) + require(linear_combination(square, gram, -13).rows == matrix([[0]*104 for _ in range(104)]).rows, + "rational inverse witness for I-A") + + kernel = [-b2[i][0] for i in range(8)]+[2]+[0]*95 + require(any(kernel) and apply_numerator(gram, kernel) == [0]*104, "nonzero Gram-kernel residual") + encoded_kernel = apply_numerator(upper, kernel) + require(encoded_kernel[:8] == [0]*8 and encoded_kernel[8] != 0, + "kernel information retained outside pivot query") + require(apply_numerator(linear_combination(identity, gram, -1), kernel) + == [entry << linear_combination(identity, gram, -1).exponent for entry in kernel], + "omitted identity-side separating residual") + + wrong_moment = times(upper_t, upper) + wrong_coded_lower = [[unit, []], [tensor_product(pivot, wrong_moment), unit]] + controls = { + "wrong_transpose_order": nonzero_blocks(coded_lower, wrong_coded_lower, "wrong M order must differ"), + "reversed_stage_order": nonzero_blocks(reference_pair, block_times(lower, upper_stage), + "Gram stage order must differ"), + "omitted_lower_identity_side": nonzero_blocks(completed_lower, coded_lower, + "Gram lower is not identity lower"), + "omitted_upper_identity_side": nonzero_blocks(completed_upper, coded_upper, + "Gram upper is not identity upper"), + } + return {"actual_ports": 104, "data_coordinates": 21632, "bank_block_entries": 10816**2, + "coefficient_domain": "real dyadic matrices; applies separately to Gaussian components", + "global_block_identities": 8, "identity_side_rank_per_bank": 10816, + "negative_control_norms": controls, "native_supplier_admitted": False, "new_kappa": False} + + +if __name__ == "__main__": + print("PASS_INDEPENDENT_P104_TENSOR_WORD_AUDIT " + json.dumps(audit(), sort_keys=True)) diff --git a/research/p104-tensor-word-audit/source/PROOF.md b/research/p104-tensor-word-audit/source/PROOF.md new file mode 100644 index 0000000000..b570c8bdf5 --- /dev/null +++ b/research/p104-tensor-word-audit/source/PROOF.md @@ -0,0 +1,201 @@ +# One dyadic code across both P104 axes + +## Question and exact scope + +PR3961 found that separately chosen row and reversed-column residual encodings +need not match. This package changes that premise: use **one invertible code on +all 21,632 data fields**, kept through both logical stages. The code is explicit, +dyadic, determinant one, preserves every independent syndrome/payload coordinate, +and has fixed X/Y return slots. It never divides by 13 or projects away a kernel. + +The canonical native-channel proof supplies the exact uncorrected endpoint +`Y += A X`, where `A=Gram/2`, sources and all 72 dirty helpers restored. The +retained copied-center caller requires an identity shear, followed by an inverse +identity shear and its physical correction/wrappers. Therefore the uncorrected +Gram experiment below is a **changed intermediate protocol**, not that completed +caller. Its scalar savings for repeated Gram pairs are not full-caller savings. +We derive the missing identity corrections explicitly rather than price them zero. + +## Dyadic triangular congruence and a global payload code + +Order the eight pivot ports `0,1,3,6,22,31,93,103` before the other 96. The pinned +fixture reconstructs `B` with 384 signed-half entries and `BB^t=12I_8`. Put + +``` +U = [ I B ] P = [ I 0 ] A = U^t P U. + [ 0 I ] [ 0 0 ] + +U^-1 = [ I -B ] M = U U^t = [ 13I B ] + [ 0 I ] [ B^t I ]. +``` + +All these U changes and inverses are over `R=Z[i,1/2]`; `det U=1`. Write +`U_r=U tensor I`, `U_c=I tensor U`, and similarly for A/P/M. On two 104 by 104 +banks define + +``` +L = U_r U_c^-t, +C = diag(L,L^-t), +Xhat=L X, Yhat=L^-t Y. +``` + +Row and column operators commute because they act on different port factors. +Neither code changes the bank names nor uses PR3882's cross-bank Pi permutation. +This is a replacement protocol; it cannot be inserted after the old literal +Pi occupancy without an additional derived and paid bridge. + +For lower and upper uncorrected Gram shears, + +``` +S_r = [I 0; A_r I], R_c = [I -A_c; 0 I], + +C S_r C^-1 = [I 0; P_r M_c I], +C R_c C^-1 = [I -M_r P_c; 0 I]. +``` + +For example, +`L^-t A_r L^-1=(U_r^-t A_r U_r^-1)(U_c U_c^t)=P_r M_c`. +The upper identity follows from `U_c^-t A_c U_c^-1=P_c`. +The same C occurs at both sides of the internal boundary: there is no row-code +to column-code transition there. This is an exact Gaussian-dyadic logical +protocol, including arbitrary real and imaginary input components. + +All data are retained. In one axis, a kernel input `(-B z,z)` becomes `(0,z)` +under U, so zero query does not mean zero payload. The decoder restores this +input exactly. Both 72-per-fiber auxiliary banks may be appended as independent +identity blocks. No helper initialization, erasure, borrowing or return is used +by this scalar code. Their required physical completion remains separate. + +## Physical operator order and fixed returns + +Let `G_0,G_1,G_2` be the actual all-role chart maps at the entrance, shared +interstage cut and exit of a proposed implementation. The retained caller gives +`G_0=diag(T,I)` and `G_2=diag(F,E)` on data, with `E=F T^-1`; its actual +intermediate owner/chart schedule is not supplied for this changed P104 protocol. +Define the physical coding map at a cut by + +``` +C_t = G_t C G_t^-1. +``` + +For a physical first stage `W1=G_1 S_r G_0^-1` and second stage +`W2=G_2 R_c G_1^-1`, the exact coded replacements are + +``` +W1hat = C_1 W1 C_0^-1 = G_1 C S_r C^-1 G_0^-1, +W2hat = C_2 W2 C_1^-1 = G_2 C R_c C^-1 G_1^-1. +``` + +For the retained data entrance and exit charts specifically, + +``` +C_0 = diag(T L T^-1, L^-t), +C_2 = diag(L, T^-1 L^-t T), +C_2^-1 = diag(L^-1, T^-1 L^t T). +``` + +Here F is common to every port and commutes with scalar port coefficients and +the positive T family. For instance, the X entry block has matrix coefficient +`T_i L_ij T_j^-1`; it is not a free scalar L_ij read across unequal charts. +At a genuinely common FULL cut, `G=diag(F,F)` and `C_t=C`; this is a useful +special case, but does not supply the missing intrinsic-source entrance. + +Their internal factors cancel in their displayed order. Port-dependent T need +not commute with U or L; no such commutation is used. The independent checker +uses noncommuting chart matrices as a control. Entry coding `C_0` and final +decoding `C_2^-1` restore the original named physical X/Y slots. Helpers are +identity blocks in C; their G maps are retained, not silently completed for free. + +These formulas specify a physical changed-caller contract. They do **not** +provide legal native recipes, shared ownership, a concrete G_1, paid cross-port +routes, or an actual adjacent completed P104 pair. Applying the bare scalar C +in physical storage would generally be wrong. Native lowering must implement +these ordered conjugates or derive an equivalent paid schedule. + +## Constructive scalar words and their complete comparison + +All counts in this section assume a common full chart, arbitrary Gaussian-dyadic +payloads, and temporarily writable donors restored after each sweep. A U or +U^-1 sweep halves 96 nonpivot donors, performs 384 signed unit ADD/SUBs and +restores by doubling. A transposed sweep uses eight pivot donors. There are no +fresh scratch arrays, cross-bank swaps, or discarded payloads. + +To encode both banks, execute four sweeps across 104 fibers each. Decode by +reversing and negating the sweeps. To apply `P_r M_c`, only eight pivot row fibers +are active: transform the source by `M=UU^t` (two sweeps), add its 104 fields +to the target row, and reverse the two sweeps. Apply `M_r P_c` analogously on +eight pivot column fibers. Every modified source is restored before the next +stage. An explicit uncoded reference computes `A=U^t P U` by a query sweep, +eight pivot deliveries, a B^t delivery, and inverse query sweep for each of +104 fibers. It is a specified constructive comparator, not an optimal word. + +| Exact scalar word | Unit ADD/SUB | Halves | Restoring doubles | +|---|---:|---:|---:| +| Global entry plus exit code | 319,488 | 43,264 | 43,264 | +| One coded **uncorrected Gram** pair | 26,240 | 3,328 | 3,328 | +| One uncoded reference Gram pair | 241,280 | 41,600 | 41,600 | + +For k repeated identical uncorrected Gram pairs, encoded ADD cost is +`319488+26240k`, compared with `241280k`; halve and double counts are each +`43264+3328k`, compared with `41600k`. One pair costs 104,448 more additions. +The first integer k giving savings in all three columns is k=2, saving 110,592 +additions and 33,280 halves and doubles each. This example demonstrates what +an amortized common code can remove: repeated query traversals on 96 nonpivot +fibers, with all entry/exit work charged. An actual repeated physical consumer +has not been identified. Other uncoded factorizations can amortize as well; +no scalar optimum, runtime speedup or native rank saving follows. + +## Identity completion restores a full-dimensional obligation + +Let `N=M^-1=U^-t U^-1`. The corrected identity shears require + +``` +C [I 0; I I] C^-1 = [I 0; N_r M_c I], +C [I -I; 0 I] C^-1 = [I -M_r N_c; 0 I]. +``` + +Hence the omitted lower/upper side terms are +`(N_r-P_r)M_c` and `M_r(N_c-P_c)`. Since +`N-P=U^-t (I-A) U^-1`, and A has eigenvalues 13 (multiplicity eight) and +zero (multiplicity 96), `I-A` is invertible. Each global side term therefore +has full rational rank **10,816**. That is algebraic rank, not a native-child +cost lower bound. In particular, compressing the Gram query to eight pivot +coordinates does not complete the required identity shear on the other 96 +independent payload coordinates. + +The complete physical bill remains + +``` +entry/exit native code + coded Gram stages + identity-side completion ++ copied-center physical endpoint correction and wrappers ++ dirty-helper completion + ownership/holding/routing/control ++ precision/recovery/admission costs. +``` + +Only the formal scalar code/Gram terms above are constructively counted here. +Every other displayed term is unresolved; none is zero by default. Reusing +PR3954's unchanged 208 mass-2576 local calls and progress assumptions retains +its 44,096 excess before added code costs. Replacing those words by this code +changes their native profile and needs a newly derived full gate. The scalar +k=2 comparison does not certify such a gate. Stop dependent native expansion +until one physical repeated consumer and its complete allowance are specified. + +## Why a free 13-eigenvalue split is invalid over the dyadic ring + +The congruence does not give a dyadic similarity to `13P`. Reduce R into F_13 +by `i -> 5` and `1/2 -> 7`. Invertible matrices over R remain invertible after +this reduction because their inverses reduce too. The Gram matrix satisfies +`A^2=13A` but has rank eight modulo 13: `V=[I B]` is surjective and V^t +injective, so `A=V^t V` has rank eight even though its square is zero. +Consequently `A_r A_c=A tensor A` has rank 64 modulo 13 and is nonzero. + +For any invertible bank-separate code `(Xhat,Yhat)=(Q X,R Y)`, the two shear +coefficients become `R A_r Q^-1` and `Q A_c R^-1`; their product is similar +to `A_r A_c`. They cannot both become scaled coordinate projectors +`alpha P_r`, `beta P_c` with `alpha beta=169`: that product reduces to zero +modulo 13, contradicting rank 64. The product 169 is forced if these are the +claimed nonzero spectral blocks. This obstruction covers bank-separate +R-invertible codes and this specific full spectral-normalization target. +It does not prohibit all joint codes, general bank-mixing programs, paid +non-dyadic primitives, or other changed graphs. Our explicit U code succeeds +by retaining the nontrivial M couplings. diff --git a/research/p104-tensor-word-audit/source/README.md b/research/p104-tensor-word-audit/source/README.md new file mode 100644 index 0000000000..be374d54df --- /dev/null +++ b/research/p104-tensor-word-audit/source/README.md @@ -0,0 +1,78 @@ +# One dyadic tensor code across both P104 axes + +This package constructs one invertible code on all **21,632 data fields**: +`L=U_r U_c^-t`, `(Xhat,Yhat)=(L X,L^-t Y)`, with +`U=[[I,B],[0,I]]`. The same code is retained across both logical Gram stages, +so the row/column representation mismatch in [PR3961](https://github.com/CrocSwap/integer-mult-bounds/pull/3961) +is replaced by a matched shared representation. Every independent payload, +including the Gram kernel, is retained; entry and exit return fixed X/Y slots. +No division by 13, scratch array, helper erasure or free owner relabel is used. + +The exact transformed Gram coefficients are `P_r M_c` and `M_r P_c`, where +`M=UU^t`. Literal scalar words and both code boundaries are fully counted. +For two **repeated uncorrected Gram pairs** they save 110,592 unit additions +and 33,280 halves/restoring doubles each against the specified uncoded word. +One pair loses 104,448 additions. This is an exact common-chart protocol +comparison, **not a full-caller, native-rank or runtime improvement**. + +The actual retained caller requires identity shears. With `N=M^-1`, their +coded coefficients become `N_r M_c` and `M_r N_c`; the omitted side terms each +have full rational rank 10,816. Algebraic rank is not native tariff. Native +transport, actual repeated consumer, identity completion, helpers, ownership +and precision remain unpriced. No complete gate passes on the present evidence. + +A separate coefficient-ring result explains why M cannot simply be discarded: +`A tensor A` has rank 64 modulo 13, while a proposed fully normalized spectral +projector product `169 P_r P_c` is zero there. Thus invertible bank-separate +Gaussian-dyadic codes cannot perform that particular free spectral split. +This does not prohibit arbitrary joint codes or programs with a changed alphabet. + +See [PROOF.md](PROOF.md) for the physical chart-conjugation order, constructive +words, full obligation ledger and scoped module proof. [RESULT.json](RESULT.json) +contains finite counts; [TASK.json](TASK.json) records the changed premise and +next questions. Selected frontier and frozen predecessors are unchanged. + +## Reproduce + +Standard-library Python 3.12: + +``` +python3.12 -B scripts/research_package.py --package research/p104-tensor-code +python3.12 -B scripts/check_research_commit.py --package research/p104-tensor-code --check-source-history +``` + +The primary verifier authenticates three canonical-main inputs, reconstructs +the P104 matrix, executes the complete encoder/two-pair/decoder scalar word on +an arbitrary dense fixture with dirty-helper sentinels, enumerates every charged +operation, and checks the modular ranks. The separate Fraction oracle imports +only the word builders, evaluates them independently on every basis column of +two small whole-grid fixtures, and checks the tensor and physical-chart formulas. +It does not import the primary evaluator or claimed receipt. Destructive tests +cover optimized execution, false typed receipts, corrupted/missing source, +readonly Git-free replay and altered operation/return behavior. Finite evidence +supports the displayed algebra; no human or kernel theorem review is claimed. + +## Open next questions + +Find one actual repeated producer/consumer pair that can retain this shared code +through the **identity completion**, and specify every intermediate physical +chart/owner. Begin with the explicit `N-P` side maps, not an eight-coordinate +restriction of the input domain. Alternatively, derive one native triangular +code sweep with exact chart transport, fixed returns and a complete allowance. +Do not expand native construction until that allowance is favorable. A new +non-dyadic alphabet or general bank-mixing code must state its changed contract +before invoking the modulo-13 result. + +## Credit + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +PR3961 supplies the preceding mismatch question; its source authentication/root +constructor is reused here with credit. PR3882/3940/3943/3954 retain the residual, +caller, cleanup and gate lineage. ToikY/PR3956 owns the adapter comparison and +PR3966 the independent uniform-phase gauge; neither is a premise of this replay. +Rohan Arun/PR1972, Chafik Boukhalfa/PR1991, Adam Gall/PR1940, Josie Elliston/E8, +Sagar Thakrar/PR1012, Douglas Colkitt, Dominik Scholz and the retained native, +compiler, occupancy and terminal-floor sources retain their original credit. +The code is newly derived; it does not claim their native word as implemented +in coded coordinates. Pending PRs are context only: all replay inputs and +provenance are on canonical main, so no unmerged Git object is required. diff --git a/research/p104-tensor-word-audit/source/verify.py b/research/p104-tensor-word-audit/source/verify.py new file mode 100644 index 0000000000..7b81946424 --- /dev/null +++ b/research/p104-tensor-word-audit/source/verify.py @@ -0,0 +1,201 @@ +#!/usr/bin/env python3 +"""Exact dyadic tensor-code protocol and coefficient-ring audit; standard library, Apache-2.0.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PIVOTS = (0, 1, 3, 6, 22, 31, 93, 103) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + def pairs(items): + ans = {} + for key, value in items: + require(key not in ans, 'duplicate JSON key') + ans[key] = value + return ans + return json.loads(path.read_text(), object_pairs_hook=pairs) + + +def authenticate(): + for row in read(HERE / 'SOURCES.json')['files']: + if row['usage'] != 'input': + continue + path = ROOT / row['path'] + require(not path.is_symlink(), 'source symlink') + data = path.read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input hash: ' + row['path']) + require(hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() == row['git_blob'], 'input blob') + + +def source_matrix(): + roots = [] + for a, b in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[a], row[b] = 2, 2 * sign + roots.append(tuple(row)) + roots.extend((1,) + tail for tail in itertools.product((-1, 1), repeat=7) if tail.count(-1) % 2 == 0) + fixture = read(ROOT / 'research/p104-native-channel/inputs/P104-FIXTURE.json')['section4_explicit_P104'] + removed = {tuple(row) for row in fixture['F0'] + fixture['C']} + ports = sorted(set(roots) - removed) + require(len(ports) == 104, 'P104 port count') + order = list(PIVOTS) + [i for i in range(104) if i not in PIVOTS] + ports = [ports[i] for i in order] + gram = [[sum(x*y for x,y in zip(a,b)) for b in ports] for a in ports] + require(all(gram[i][j] == 8*(i == j) for i in range(8) for j in range(8)), 'pivot Gram') + b2 = [[gram[i][j] // 4 for j in range(8,104)] for i in range(8)] + require(all(v in (-1,0,1) for row in b2 for v in row), 'signed half coefficients') + require(all(sum(b2[i][k]*b2[j][k] for k in range(96)) == 48*(i == j) for i in range(8) for j in range(8)), 'BBt=12I') + require(all(sum(b2[k][i]*b2[k][j] for k in range(8)) == gram[i+8][j+8]//2 for i in range(96) for j in range(96)), 'nonpivot Gram') + return b2 + + + +def index(bank,i,j,n): return (bank*n+i)*n+j + + +def triangular(b,bank,axis,fixed,transpose=False,inverse=False): + p=len(b);n=p+len(b[0]) + def ix(k): return index(bank,k,fixed,n) if axis==0 else index(bank,fixed,k,n) + donors=range(p) if transpose else range(p,n) + for d in donors: yield ('half',ix(d)) + for j,row in enumerate(b): + for k,v in enumerate(row,p): + if v: + dest,src=(k,j) if transpose else (j,k) + yield ('add',ix(dest),ix(src),-v if inverse else v) + for d in donors: yield ('double',ix(d)) + + +def code_word(b,inverse=False): + n=len(b)+len(b[0]) + steps=[(0,1,True,True),(0,0,False,False),(1,1,False,False),(1,0,True,True)] + if inverse: steps=[(bank,axis,t,not inv) for bank,axis,t,inv in reversed(steps)] + for bank,axis,t,inv in steps: + for fixed in range(n):yield from triangular(b,bank,axis,fixed,t,inv) + + +def coded_pair(b): + p=len(b);n=p+len(b[0]) + # lower: Y += P_r M_c X. upper: X -= M_r P_c Y. + for source,axis in ((0,1),(1,0)): + target=1-source;sign=1 if source==0 else -1 + for fixed in range(p): + yield from triangular(b,source,axis,fixed,True) + yield from triangular(b,source,axis,fixed) + for k in range(n): + i,j=(fixed,k) if axis==1 else (k,fixed) + yield ('add',index(target,i,j,n),index(source,i,j,n),sign) + yield from triangular(b,source,axis,fixed,inverse=True) + yield from triangular(b,source,axis,fixed,True,True) + + +def reference_pair(b): + p=len(b);n=p+len(b[0]) + for source,axis in ((0,0),(1,1)): + target=1-source;sign=1 if source==0 else -1 + for fixed in range(n): + def ix(bank,k):return index(bank,k,fixed,n) if axis==0 else index(bank,fixed,k,n) + yield from triangular(b,source,axis,fixed) + for j in range(p):yield ('add',ix(target,j),ix(source,j),sign) + for j in range(p):yield ('half',ix(source,j)) + for j,row in enumerate(b): + for k,v in enumerate(row,p): + if v:yield ('add',ix(target,k),ix(source,j),sign*v) + for j in range(p):yield ('double',ix(source,j)) + yield from triangular(b,source,axis,fixed,inverse=True) + + +def evaluate(word,values): + x=list(values) + for op in word: + if op[0]=='add':x[op[1]]+=op[3]*x[op[2]] + elif op[0]=='half': + require(x[op[1]]%2==0,'exact dyadic integer test scale') + x[op[1]]//=2 + elif op[0]=='double':x[op[1]]*=2 + else:raise ValueError('unknown operation') + return x + + +def invoice(word): + from collections import Counter + c=Counter(op[0] for op in word) + return {key:c[key] for key in ('add','half','double')} + + +def mod_rank(a,p=13): + a=[[x%p for x in row] for row in a];r=0 + for j in range(len(a[0])): + pivot=next((i for i in range(r,len(a)) if a[i][j]),None) + if pivot is None:continue + a[r],a[pivot]=a[pivot],a[r];scale=pow(a[r][j],-1,p);a[r]=[(x*scale)%p for x in a[r]] + for i in range(len(a)): + if i!=r: + c=a[i][j];a[i]=[(v-c*w)%p for v,w in zip(a[i],a[r])] + r+=1 + if r==len(a):break + return r + + +def result(): + authenticate();b=source_matrix();n=104;p=8 + enc=list(code_word(b));dec=list(code_word(b,True));cp=list(coded_pair(b));rp=list(reference_pair(b)) + ei=invoice(enc+dec);ci=invoice(cp);ri=invoice(rp) + require(ei=={'add':319488,'half':43264,'double':43264},'boundary invoice') + require(ci=={'add':26240,'half':3328,'double':3328},'coded pair invoice') + require(ri=={'add':241280,'half':41600,'double':41600},'reference pair invoice') + # Dense arbitrary integer fixture, including untouched dirty-helper sentinels. + data=[((i*37+i//11)%31-15)*(1<<24) for i in range(2*n*n)]+[123,-77] + require(evaluate(dec,evaluate(enc,data))==data,'full payload inverse') + reference=evaluate(rp,evaluate(rp,data)) + coded=evaluate(dec,evaluate(cp,evaluate(cp,evaluate(enc,data)))) + require(coded==reference,'actual P104 two-pair scalar endpoint') + require(coded[-2:]==data[-2:],'arbitrary dirty helper preservation') + # A nonzero kernel payload is retained in syndrome coordinates. + syndrome=[0]*(2*n*n) + syndrome[index(0,8,0,n)]=2 + for i in range(p):syndrome[index(0,i,0,n)]=-b[i][0] + require(any(syndrome),'nonzero syndrome') + require(evaluate(dec,evaluate(enc,[v*(1<<16) for v in syndrome]))==[v*(1<<16) for v in syndrome],'kernel payload retained') + # Reconstruct A mod13 from V=[I B], not by division by its eigenvalue. + v=[[int(i==j) for j in range(p)]+[(x*7)%13 for x in b[i]] for i in range(p)] + a=[[sum(v[k][i]*v[k][j] for k in range(p))%13 for j in range(n)] for i in range(n)] + rank=mod_rank(a) + require(rank==8 and all(sum(a[i][k]*a[k][j] for k in range(n))%13==0 for i in range(n) for j in range(n)),'nonzero square-zero mod13 Gram') + require(mod_rank(b)==8,'B mod13 rank') + v5=[[int(i==j) for j in range(p)]+[(x*3)%5 for x in b[i]] for i in range(p)] + side5=[[(int(i==j)-sum(v5[k][i]*v5[k][j] for k in range(p)))%5 for j in range(n)] for i in range(n)] + require(mod_rank(side5,5)==104,'full-rank identity side correction') + # 13*(1/13)=1 cannot hold for dyadic coefficients; 13 reduces to zero. + require(13%13==0 and pow(2,-1,13)==7 and 5*5%13==12,'ring homomorphism') + return {'schema':'p104-tensor-code/1','data_degrees':2*n*n,'source_rank':8,'mod13_gram_rank':rank,'mod13_tensor_product_rank':rank*rank,'full_identity_side_rank':n*n, + 'code':'L=U_r U_c^-t; (Xhat,Yhat)=(L X,L^-t Y)', + 'transformed_lower':'P_r M_c','transformed_upper':'M_r P_c', + 'boundary_invoice':ei,'coded_pair_invoice':ci,'reference_pair_invoice':ri, + 'one_pair_add_difference':ei['add']+ci['add']-ri['add'], + 'two_pair_add_saving':2*ri['add']-ei['add']-2*ci['add'], + 'two_pair_half_saving':2*ri['half']-ei['half']-2*ci['half'], + 'first_add_break_even_integer':2,'first_half_break_even_integer':2, + 'arithmetic_scope':'exact common-chart Gaussian dyadic word; formal scalar counts, not physical/native upper bill', + 'remaining':'physical chart recipes, actual repeated consumer, identity-side correction, helpers/owners, full native moment and precision'} + + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write-result',action='store_true');parser.add_argument('--result',type=Path,default=HERE/'RESULT.json');args=parser.parse_args() + r=result() + if args.write_result:args.result.write_text(json.dumps(r,indent=2,sort_keys=True)+'\n') + else:require(json.dumps(read(args.result),sort_keys=True)==json.dumps(r,sort_keys=True),'typed result mismatch') + print('PASS_P104_TENSOR_CODE payload=21632 mod13_rank=64 two_pair_add_saving=110592 no_new_kappa') + +if __name__=='__main__':main() diff --git a/research/p104-tensor-word-audit/test_verify.py b/research/p104-tensor-word-audit/test_verify.py new file mode 100644 index 0000000000..6e444c145b --- /dev/null +++ b/research/p104-tensor-word-audit/test_verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Literal-word semantic controls and source-bound export checks. + +Apache-2.0. Separate AI test implementation, not human/formal/native review. +Only authenticated predecessor word builders are objects under review. These +controls exercise the companion arithmetic audit without using its predecessor +execution or invoice routines. +""" +from __future__ import annotations + +import hashlib +import json +from pathlib import Path +import shutil +import stat +import subprocess +import sys +import tempfile +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = Path('research/p104-tensor-word-audit') +FIXTURE = Path('research/p104-native-channel/inputs/P104-FIXTURE.json') + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +def snapshot(root): + return {str(p.relative_to(root)): (p.stat().st_ino, stat.S_IMODE(p.stat().st_mode), + hashlib.sha256(p.read_bytes()).hexdigest()) + for p in root.rglob('*') if p.is_file()} + + +def private_fixture(root): + package = root / PACKAGE + package.parent.mkdir(parents=True) + shutil.copytree(HERE, package, copy_function=shutil.copyfile, + ignore=shutil.ignore_patterns('__pycache__', '.git')) + fixture = root / FIXTURE + fixture.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / FIXTURE, fixture) + # copytree copies directory metadata even with copyfile. Only these newly + # created private fixtures become writable; the source export stays intact. + for directory in [root] + [p for p in root.rglob('*') if p.is_dir()]: + directory.chmod(0o755) + return package + + +def execute(arguments, optimized=False, cwd=None): + command = [sys.executable, '-I', '-B'] + (['-O'] if optimized else []) + arguments + return subprocess.run(command, cwd=cwd, capture_output=True, text=True, timeout=40) + + +API_DRIVER = r''' +import runpy,sys +v=runpy.run_path(sys.argv[1]) +words,b=v['get_words']() +n=104 +count=0 + +def reject(name,key,change,expected): + global count + altered=dict(words) + altered[key]=list(words[key]) + change(altered[key]) + try: + v['certify'](words=altered) + except ValueError as error: + if expected not in str(error): + raise RuntimeError(name+' failed for an unexpected reason: '+str(error)) + else: + raise RuntimeError('accepted literal mutation: '+name) + count+=1 + +first_add=next(i for i,op in enumerate(words['enc']) if op[0]=='add') +def replace(word,index,operation): word[index]=operation + +def flip(word,index): + op=word[index] + word[index]=(op[0],op[1],op[2],-op[3]) + +def orient(word): + op=word[first_add] + word[first_add]=(op[0],op[2],op[1],op[3]) + +def interleave(word): + word[0],word[first_add]=word[first_add],word[0] + +reject('helper_index','enc',lambda w:replace(w,0,('half',2*n*n)), 'global data index') +reject('boolean_index','enc',lambda w:replace(w,0,('half',True)), 'global data index') +reject('wrong_bank','enc',lambda w:replace(w,0,('half',w[0][1]+n*n)), 'bank ownership') +reject('wrong_sign','enc',lambda w:flip(w,first_add), 'exact fiber linear map') +reject('boolean_sign','enc',lambda w:replace(w,first_add,('add',w[first_add][1],w[first_add][2],True)), 'unit sign') +reject('orientation','enc',orient, 'exact fiber linear map') +reject('half_add_interleaving','enc',interleave, 'exact fiber linear map') +# The first transposed sweep has384 additions and twice8 donor scalings. +# Damage the corresponding add only in its second fixed-coordinate instance. +reject('later_cached_fiber','enc',lambda w:flip(w,400+first_add), 'nonuniform fiber program') +reject('omitted_coded_source_restoration','coded',lambda w:w.pop(), 'truncated fiber') +reject('omitted_reference_source_restoration','reference',lambda w:w.pop(), 'truncated fiber') +reject('trailing_unaudited_operation','enc',lambda w:w.append(('double',0)), 'unconsumed encoder/decoder events') +# A literal address in another fixed-coordinate fiber cannot be relocalized silently. +reject('wrong_axis_owner','enc',lambda w:replace(w,0,('half',w[0][1]+n)), 'fiber ownership/axis') +print('PASS_LITERAL_MUTATION_CONTROLS cases='+str(count)) +''' + + +def semantic_controls(): + for optimized in (False, True): + run = execute(['-c', API_DRIVER, str(HERE / 'verify.py')], optimized, HERE) + need(run.returncode == 0 and 'PASS_LITERAL_MUTATION_CONTROLS cases=12' in run.stdout, + 'literal semantic controls failed optimized=' + str(optimized) + '\n' + run.stderr) + return 12 + + +def cli_controls(base): + names = ('changed_builder', 'missing_builder', 'changed_frozen_proof', + 'changed_fixture', 'missing_fixture', 'undercharged_invoice', 'typed_boolean_invoice') + independent_runs = 0 + for name in names: + root = base / name + package = private_fixture(root) + if name == 'changed_builder': + path = package / 'source/verify.py' + path.write_bytes(path.read_bytes() + b'\n') + elif name == 'missing_builder': + (package / 'source/verify.py').unlink() + elif name == 'changed_frozen_proof': + path = package / 'source/PROOF.md' + path.write_bytes(path.read_bytes() + b'\n') + elif name == 'changed_fixture': + path = root / FIXTURE + path.write_bytes(path.read_bytes() + b'\n') + elif name == 'missing_fixture': + (root / FIXTURE).unlink() + else: + path = package / 'CERTIFICATE.json' + cert = json.loads(path.read_text()) + if name == 'undercharged_invoice': + cert['invoices']['boundary']['add'] -= 1 + else: + cert['schema_version'] = True + path.write_text(json.dumps(cert)) + for optimized in (False, True): + run = execute([str(package / 'verify.py')], optimized, root) + need(run.returncode != 0 and + ('ValueError' in run.stderr or 'FileNotFoundError' in run.stderr), + 'damaged actual CLI accepted or crashed unexpectedly: ' + name + '\n' + run.stderr) + if name in ('changed_fixture', 'missing_fixture'): + other = execute([str(package / 'independent.py')], optimized, root) + need(other.returncode != 0 and + ('ValueError' in other.stderr or 'FileNotFoundError' in other.stderr), + 'independent CLI accepted damaged canonical fixture: ' + name) + independent_runs += 1 + return len(names), independent_runs + + +def readonly_positive(base): + root = base / 'readonly' + package = private_fixture(root) + files = [p for p in root.rglob('*') if p.is_file()] + directories = [root] + [p for p in root.rglob('*') if p.is_dir()] + for path in files: + original = (HERE / path.relative_to(package)) if path.is_relative_to(package) else ROOT / path.relative_to(root) + need(path.stat().st_ino != original.stat().st_ino, 'shared read-only fixture inode') + path.chmod(0o444) + for path in directories: + path.chmod(0o555) + before = snapshot(root) + try: + for optimized in (False, True): + run = execute([str(package / 'verify.py')], optimized, root) + need(run.returncode == 0 and run.stdout.startswith('PASS_P104_TENSOR_WORD_AUDIT '), + 'full readonly actual104 CLI failed: ' + run.stderr) + result = json.loads(run.stdout.split(' ', 1)[1]) + need(result['ports'] == 104 and result['data_degrees'] == 21632 + and result['audited_literal_operations'] == 763392 + and result['fiber_instances'] == 1056 and result['distinct_exact_local_maps'] == 8, + 'positive literal coverage changed') + need(snapshot(root) == before, 'read-only export changed') + finally: + for path in sorted(directories, key=lambda p:len(p.parts)): + path.chmod(0o755) + return len(files) + + +def main(): + started = time.monotonic() + original = snapshot(HERE) + original_fixture = (ROOT / FIXTURE).read_bytes() + api = semantic_controls() + with tempfile.TemporaryDirectory(prefix='p104-tensor-word-controls-') as temporary: + base = Path(temporary) + cli, independent_runs = cli_controls(base) + readonly_files = readonly_positive(base) + need(snapshot(HERE) == original and (ROOT / FIXTURE).read_bytes() == original_fixture, + 'source package or canonical fixture changed') + print('PASS_P104_TENSOR_WORD_CONTROLS semantic_cases=' + str(api) + + ' cli_cases=' + str(cli) + ' negative_runs=' + str(2*(api+cli)) + + ' independent_source_negative_runs=' + str(independent_runs) + + ' actual104_normal_optimized=PASS readonly_git_free_files=' + str(readonly_files) + + ' source_unchanged=PASS elapsed_seconds=' + format(time.monotonic()-started,'.3f')) + + +if __name__ == '__main__': + main() diff --git a/research/p104-tensor-word-audit/verify.py b/research/p104-tensor-word-audit/verify.py new file mode 100644 index 0000000000..545f1095d9 --- /dev/null +++ b/research/p104-tensor-word-audit/verify.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Exact disjoint-fiber audit of frozen PR3979 word builders. Apache-2.0.""" +from __future__ import annotations +from collections import Counter +from fractions import Fraction as Q +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +PINS={'README.md':'7c57cda30963c1fc37a96b92182912b3942e4e2447ba599db9f7af2359414d9c', + 'PROOF.md':'259ba7b0926dd6db4e7c45ff7ccb10659dee06aef0a573547236c994ad304756', + 'verify.py':'27bae82fe247fe49b8fc3b5efbd429e2c8c0ee8f56cc4ace748cbb681a5abacc'} +FIXTURE='research/p104-native-channel/inputs/P104-FIXTURE.json' +FIXTURE_SHA='516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4' +B2_SHA='88e9a726e8c8aec055bfd7cd024883b5c8ecbda0cd6471e591a08c43a108a535' + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def unique(pairs): + d={} + for k,v in pairs: + need(k not in d,'duplicate JSON key');d[k]=v + return d + + +def load(path):return json.loads(path.read_text(),object_pairs_hook=unique) + + +def authenticate(): + for path,digest in [(HERE/'source'/n,s) for n,s in PINS.items()]+[(ROOT/FIXTURE,FIXTURE_SHA)]: + need(not path.is_symlink(),'source symlink') + need(hashlib.sha256(path.read_bytes()).hexdigest()==digest,'source bytes: '+str(path)) + + +def get_words(): + authenticate() + spec=importlib.util.spec_from_file_location('frozen_3979_word_builders',HERE/'source/verify.py') + module=importlib.util.module_from_spec(spec);spec.loader.exec_module(module) + # Relocate only its canonical fixture root. No source bytes are changed and + # no predecessor evaluator, result(), invoice or claimed receipt is called. + module.ROOT=ROOT + b=module.source_matrix() + return ({'enc':list(module.code_word(b)), 'dec':list(module.code_word(b,True)), + 'coded':list(module.coded_pair(b)), 'reference':list(module.reference_pair(b))},b) + + +def eye(n):return [{i:Q(1)} for i in range(n)] + + +def transpose(a): + out=[{} for _ in a] + for i,row in enumerate(a): + for j,v in row.items():out[j][i]=v + return out + + +def multiply(a,b): + out=[] + for row in a: + d={} + for k,v in row.items(): + for j,w in b[k].items():d[j]=d.get(j,Q(0))+v*w + out.append({j:v for j,v in d.items() if v}) + return out + + +def interpret(word,size): + rows=eye(size) + for op in word: + need(isinstance(op,(tuple,list)) and op,'operation tuple') + kind=op[0] + need(kind in ('add','half','double'),'operation alphabet') + need(len(op)==(4 if kind=='add' else 2),'operation arity') + need(type(op[1]) is int and 0<=op[1]