diff --git a/research/native-coupled-inverse/ORIGINS.json b/research/native-coupled-inverse/ORIGINS.json new file mode 100644 index 0000000000..781095ae20 --- /dev/null +++ b/research/native-coupled-inverse/ORIGINS.json @@ -0,0 +1,56 @@ +{ + "head": "3348fccea855082786d5f0fc5558b73d4974e745", + "repository": "CrocSwap/integer-mult-bounds", + "pr": 5402, + "archive_sha256": "530fe35e8e8abdcf9c6207168c7e8586c56b2fbe491c6c67046bea83343809cc", + "files": [ + { + "file": "verify.py", + "path": "research/native-rank8-helper-provider/verify.py", + "git_blob": "b62af49c87864ad9337f3964b2515ba53de85d4f", + "sha256": "121d87787c0f76bd530b6e1682704a311e96dfb33d787bea2ba29a1d0e5ee23e" + }, + { + "file": "README.md", + "path": "research/native-rank8-helper-provider/README.md", + "git_blob": "92d0d7e523dbf90c67b7244de4c87cc74c0d3b61", + "sha256": "0d86590c471a498f3b735397d42bbaf4d5e89c33b75ddbd48dbf972192ab351f" + }, + { + "file": "PROOF.md", + "path": "research/native-rank8-helper-provider/PROOF.md", + "git_blob": "5cbfc4fd02dce926c3d235f1549bdb2035dea088", + "sha256": "2d59282f3b5e9fb848d0099ce91729fa433162e6975f877a441e2ab4f57a29c5" + }, + { + "file": "ATTRIBUTION.md", + "path": "research/native-rank8-helper-provider/ATTRIBUTION.md", + "git_blob": "efe3acb566448caeb4a340235bb50234808ff728", + "sha256": "29756f86ebad2a957d8073bea173306f00e7d957828a5bab9f7832faf5815543" + }, + { + "file": "SOURCES.json", + "path": "research/native-rank8-helper-provider/SOURCES.json", + "git_blob": "dd77397ca519f0c15799b4f90a489af3d6a2cb0f", + "sha256": "f16756004bd3100e4993b250181c4c8d15c31b0a1478b627091dd900e1103888" + }, + { + "file": "WITNESS.json", + "path": "research/native-rank8-helper-provider/WITNESS.json", + "git_blob": "19665f9eac2238d709758e0296eb6016e71b2b1a", + "sha256": "24599011da06325e1012619b2b84a4dd3aceb90ab42d3caaf6414879e7d16591" + }, + { + "file": "PROVIDER.json", + "path": "research/native-rank8-helper-provider/PROVIDER.json", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, + { + "file": "WORD.json.gz", + "path": "research/native-rank8-helper-provider/WORD.json.gz", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + } + ] +} diff --git a/research/native-coupled-inverse/PROOF.md b/research/native-coupled-inverse/PROOF.md new file mode 100644 index 0000000000..1d524fb69d --- /dev/null +++ b/research/native-coupled-inverse/PROOF.md @@ -0,0 +1,165 @@ +# A native inverse with the same paid Gaussian profile + +This construction inverts the coupled provider from +[PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402), at +`3348fccea855082786d5f0fc5558b73d4974e745`. It preserves all 632 original +input directions. Nine temporary fields can start with arbitrary values and +finish zero. No new Gaussian child is needed. The inverse needs additional +ordinary operations, which are counted below. + +This is an enabling construction. It gives no new kappa, complete caller, +autonomous credit for the eight coupled outputs, or selected-result change. +The physical source implementation and its interpretation at every positive +fiber width remain inherited premises. The source replay is run again. + +## Exact physical map + +Use the source notation. Q is the central Gaussian, D is the product on the +eight other axes, and R = DQ. W and Z are the specified ordinary maps between +112 main fields and eight mode fields. They satisfy ZW = 14I, WZ = I - C, +RW = WR, and RZ = ZR, with the appropriate domain on each side. Do not commute +W or Z through D or Q separately. + +The source map is + +```text +X = D x - R y + R W h +Y = D y +H = D(h - Z y). +``` + +Its inverse is + +```text +y = D^-1 Y +h = D^-1 H + Z D^-1 Y +x = D^-1 X + Q C D^-1 Y - Q W D^-1 H. +``` + +The first two equations give y and h. Substitution in the X equation gives +the third equation, since C = I - WZ. This derivation retains operator order. +It proves the map is invertible; it does not alone give a native schedule. +The schedule below supplies that missing implementation. The other 400 fields +undergo the inverses of their original autonomous helper maps. + +## Remove the unused center accumulator + +The changed source word has no paid operation on C0. Its live center uses have +this form, in the same chart: + +```text +CLEAR C0 +COPY C0, Ck +ADD Lr, C0, -1 +CLEAR C0 +``` + +Replace the live ADD by `ADD Lr, Ck, -1`. Delete all scalar writes to C0. +Before each replaced center, the old accumulation in C0 is erased without a +read. In total, 176 ADDs, eight COPYs and 24 CLEARs are removed. The eight +source sites and their cache fields are in RESULT.json. One entry CLEAR keeps +the unused C0 field zero under the retained nine-field temporary interface. + +The source interpreter checks every endpoint row, every persistent/cache +exit chart, and every paid call before and after this change. The final chart +of the unused zero C0 field is immaterial; no original field is excluded. + +The remaining word consists of invertible ADDs, nonzero SCALEs, native maps, +paid children, eight initial cache CLEAR/COPY pairs, and eight retags of +identically zero persistent fields. Each retained cache is read but not +changed until the final whole-field swap. + +## Reverse the complete word + +Reverse the physical output boundary first. Clear the nine temporary fields. +Undo each final whole-field swap, including its chart. Apply the inverse cache +normalizer and its inverse scalar. The original persistent mode field is now +zero, while the cache contains the corresponding independent output input. +Apply the inverse output helper basis, then run the reduced native word in +reverse order: + +- Negate an ADD coefficient and invert a nonzero SCALE coefficient. +- Invert a native map and reverse its chart transition. +- Invert a paid child and reverse its chart transition. Keep its rank. +- Reverse a zero retag only after its row is proved zero. +- Replace a cache COPY by subtraction of its restored source field. +- At an initial cache CLEAR, verify that its row is zero and do no operation. + +Finally invert the input helper basis and the physical input boundaries. +All eight inverse COPY operations return their cache rows to zero. Clear +the eight owned cache returns after this check. C0 stays zero. The verifier starts with 641 distinct formal input columns, erases only +owned entry dirt, and checks both compositions against the identity on the +632 original columns. It also checks the inverse endpoint against a separate +closed formula in the source scalar coordinates: + +```text +y = Y +h = H + M^T Y +x = X + (I - M M^T/4) Y - M H/4. +``` + +Here M has 112 rows and eight columns. The source file stores its transpose. +The physical boundary maps convert this formula to the ordered physical +inverse above. All 464 boundary adjoints are checked with both signed +Clifford tableaux and absolute phase. Source adapter and phase annotations +retain their physical interpretation in reverse order; they are not new +scalar row operations. Internal native maps use their actual inverses. + +For a positive rank-r Gaussian child G, `G^-1 = X G`, where X translates the +r active bits. Thus a descending child needs one rank-r positive call and at +most one additional ordinary translation. The verifier checks the exact phase +identity for ranks 1 through 9. Tensoring this identity gives the same result +at every positive fiber width. Scalar coefficients in the owner program are +applied once; the program does not tensor a sum over owners. + +Every other operation is reversed literally. The free-group row proof holds +for each evaluation of the native maps by invertible operators. This proves +the all-width inverse within the inherited native implementation model. +No formal proof kernel or independent human review is claimed. + +## Complete local bill and limits + +Both directions use the paid profile +`{1:2193, 2:412, 3:510, 4:127, 5:40}`: 3,282 child calls and rank mass 5,255. +The 400 autonomous helper jobs retain inverse Gaussian ranks +`{4:28, 7:7, 8:47, 9:318}`. The remaining eight fields are coupled; they get +no autonomous target credit. + +| Explicit operation | Reduced forward | Inverse | +|---|---:|---:| +| ADD | 17,741 | 17,749 | +| SCALE | 1,204 | 1,204 | +| COPY | 8 | 0 | +| CLEAR | 17 | 17 | +| Whole-field SWAP | 8 | 8 | +| Physical boundary monomial maps | 464 | 464 | +| Additional child-inverse translations | 0 | at most 3,282 | + +The CLEAR count includes eight terminal owned clears in each direction. +They act on certified zeros in the exact model. + +The native word's 240 internal warp records remain. Its 448 adapter and ten +phase annotations retain their source semantics. RESULT.json records their +full census. The table does not turn these inherited operations into zero +work and does not give a complete machine/compiler tariff. + +A direct product of scalar operator-norm bounds gives an inverse suffix bound +of `2^18812`. Gaussian and monomial maps have norm one. A local schedule with +m errors of norm at most epsilon therefore has output error at most +`m * 2^18812 * epsilon`. This is a conservative fixed-template bound. +The complete caller, recursive error allocation, movement, storage, compiler, +BIT supplier and outer recovery still need explicit funding. In particular, +unchanged Gaussian counts do not imply unchanged ordinary/compiler costs. + +## Verification and next use + +The registered verifier runs the frozen predecessor replay, reconstructs the +changed word, checks both all-column compositions and the separate inverse +formula, and checks owned cleanup, charts, exact paid counts, boundary phases +and inverse child phases. Mutations of inverse COPY sign, reverse zero-retag +input and boundary phase must fail. + +The next use is one chronological caller that retains useful progress in the +eight mode fields. Its full invoice must include every helper transfer and +all additional queries. A local inverse, a favorable cost estimate or a +finite failed control search does not establish that caller. diff --git a/research/native-coupled-inverse/README.md b/research/native-coupled-inverse/README.md new file mode 100644 index 0000000000..ea6786053b --- /dev/null +++ b/research/native-coupled-inverse/README.md @@ -0,0 +1,79 @@ +# Invert the eight-mode coupled native provider + +This package gives an exact native inverse of +[PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402) at +`3348fccea855082786d5f0fc5558b73d4974e745`. All 632 original input directions +are retained and all nine owned fields return zero. The inverse uses the same +paid profile: `{1:2193,2:412,3:510,4:127,5:40}`. It adds no Gaussian child. + +The construction removes the unused C0 accumulator, reverses the remaining +native operations, and uncomputes the eight retained copies by subtraction. +The complete physical boundary is reversed with its exact phase. Positive +Gaussian implementations of the inverse children need at most 3,282 additional +ordinary bit translations. These operations are explicit costs. + +**This does not increase kappa.** The eight mode outputs remain coupled. +A profitable complete caller, full compiler/precision bill and outer admission +remain open. Reversing a source operation also reverses its D factor; it does +not supply an independent fresh-D call by itself. The selected frontier is +unchanged. + +[PROOF.md](PROOF.md) gives the ordered physical inverse, all-width argument, +chronological schedule and local bill. [RESULT.json](RESULT.json) records the +exact replay receipt. The verifier runs the pinned predecessor replay, checks +both compositions on all original columns, checks a separate inverse formula, +and rejects changes to COPY sign, zero-retag input and boundary phase. +It checks 464 boundary adjoints and the phase-correct inverse-child identity +for ranks 1 through 9. No independent human or formal-kernel review is claimed. + +## Reproduce + +Python 3.12 and its standard library suffice for mathematical replay. +The optional source-history preflight also needs full Git history. From the +repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/native-coupled-inverse +python3.12 -I -O -B research/native-coupled-inverse/verify.py +python3.12 -B scripts/check_research_commit.py --package research/native-coupled-inverse --check-source-history +``` + +Expected final token: `PASS_SAME_PAID_NATIVE_TWO_SIDED_INVERSE`. +The default verifier is read-only. `--emit` writes RESULT.json for authors. +[VALIDATION.md](VALIDATION.md) records executed checks and unrun obligations. + +## Sources and credit + +Dillon supplies the coupled provider, its all-input basis and physical boundary +in [PR #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402). +The [source proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3348fccea855082786d5f0fc5558b73d4974e745/research/native-rank8-helper-provider/PROOF.md) +and [attribution](https://github.com/CrocSwap/integer-mult-bounds/blob/3348fccea855082786d5f0fc5558b73d4974e745/research/native-rank8-helper-provider/ATTRIBUTION.md) +remain part of the review. SOURCE.zip contains the exact source files needed +to replay that pending construction without a network or an unmerged Git +object. ORIGINS.json records their source paths, Git blobs and byte hashes. +The archive retains the original README, proof and attribution. It is unpacked +only to a private temporary directory. No predecessor code is changed. + +Ali Romman's [PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) +supplies the eight cached-center identities consumed by that provider. +Cao Yifan supplies the actual native word, Dugongue supplies the center-free +code, and Cinna Davis supplies the retained-cache/helper/controller lineage. +Retain zxv's native and Clifford work, Jacob Alan Sussman's mixed-target +recursion, Ryanson Jonathan's controller checks and the full source notices. +Yiyang's [PR #4966](https://github.com/CrocSwap/integer-mult-bounds/pull/4966) +already constructs owned-center inverses for the original word by recomputation. +This result uses the new retained-cache interface and its eight zero outputs; +it does not claim the first native inverse or the general idea of uncomputation. + +Canonical base: `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7. +The [caller claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19156336) +takes Dillon's released handoff. The broader breakthrough goal is not complete. +New inverse construction, proof and checks prepared for Ali Romman with +substantial OpenAI Codex assistance. No subagents. Apache-2.0. + +## Open next questions + +Use the exact inverse to close one chronological caller that preserves useful +progress in the eight mode fields. First give every original endpoint and the +full paid/ordinary invoice. Only then run compiler, precision and outer +admission. [TASK.json](TASK.json) records this question and its open obligations. diff --git a/research/native-coupled-inverse/RESULT.json b/research/native-coupled-inverse/RESULT.json new file mode 100644 index 0000000000..97da48b662 --- /dev/null +++ b/research/native-coupled-inverse/RESULT.json @@ -0,0 +1,130 @@ +{ + "status": "PASS_SAME_PAID_NATIVE_TWO_SIDED_INVERSE", + "source_pr": 5402, + "source_head": "3348fccea855082786d5f0fc5558b73d4974e745", + "independent_original_columns": 632, + "owned_outputs_zero": 9, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "removed_dead_C0_records": { + "clear": 24, + "add": 176, + "copy": 8 + }, + "live_cache_substitutions": [ + [ + 11350, + [ + "C", + 1 + ] + ], + [ + 11377, + [ + "C", + 2 + ] + ], + [ + 11404, + [ + "C", + 3 + ] + ], + [ + 11431, + [ + "C", + 4 + ] + ], + [ + 11458, + [ + "C", + 5 + ] + ], + [ + 11485, + [ + "C", + 6 + ] + ], + [ + 11512, + [ + "C", + 7 + ] + ], + [ + 11539, + [ + "C", + 8 + ] + ] + ], + "inverse_copy_uncomputations": [ + 640, + 639, + 638, + 637, + 636, + 635, + 634, + 633 + ], + "inherited_record_types": { + "phase": 10, + "warp": 240, + "scalar": 17485, + "adapter": 448, + "climb": 3282, + "zero_retag": 8 + }, + "boundary_adjoint_checks": 464, + "inverse_child_ranks_checked": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "ordinary_forward": { + "add": 17741, + "scale": 1204, + "clear": 17, + "copy": 8, + "swap": 8, + "monomial": 464 + }, + "ordinary_inverse": { + "add": 17749, + "scale": 1204, + "clear": 17, + "swap": 8, + "monomial": 464, + "child_inverse_translation": 3282 + }, + "inverse_local_amplification_power2_bound": 18812, + "failure_controls": [ + "wrong inverse COPY sign rejected", + "nonzero reverse retag rejected", + "same-tableau inverse phase error rejected" + ], + "scope": "All-width native inverse of the coupled provider; no autonomous credit for the coupled outputs, complete caller, full precision/compiler bill or new kappa." +} diff --git a/research/native-coupled-inverse/SOURCE.zip b/research/native-coupled-inverse/SOURCE.zip new file mode 100644 index 0000000000..3b54e49e0b Binary files /dev/null and b/research/native-coupled-inverse/SOURCE.zip differ diff --git a/research/native-coupled-inverse/SOURCES.json b/research/native-coupled-inverse/SOURCES.json new file mode 100644 index 0000000000..dd77397ca5 --- /dev/null +++ b/research/native-coupled-inverse/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/coded-native-caller/PHYSICAL.md", + "usage": "input", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + { + "path": "research/coded-native-caller/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/native-center-free-code/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "path": "research/native-center-free-code/CODED-PROOF.md", + "usage": "input", + "git_blob": "1f28d33884ec99b34f8366d022d8f7b9b7653ae2", + "sha256": "acd904af677718da8cdaf81d205d29866a6855efd393047e7128320a46753b01" + }, + { + "path": "research/native-center-free-code/SOURCE-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + } + ] +} diff --git a/research/native-coupled-inverse/TASK.json b/research/native-coupled-inverse/TASK.json new file mode 100644 index 0000000000..46f72864ea --- /dev/null +++ b/research/native-coupled-inverse/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct the inverse of the PR5402 coupled native provider at the same paid profile, with all 632 original inputs and owned cleanup.", + "scope_change_reason": "The released complete-caller handoff needs a source-native inverse. This package closes that primitive obligation and does not claim a profitable complete caller.", + "bottleneck_link": "An exact inverse permits chronological compositions of the retained eight-mode interface. The caller and full kappa calculation remain open.", + "budget_minutes": 60, + "stop_rule": "Reject any changed paid child, nonzero owned return, unbound source operation or incomplete inverse endpoint.", + "outcome": "completed", + "evidence": "Two-sided exact all-column native replay, independent inverse formula, source replay, child-inverse identities and rejection controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents.", + "open_questions": [ + { + "question": "Can the coupled provider and this inverse close a caller that retains useful shared helper progress?", + "why_it_matters": "The local center savings do not improve kappa until all coupled outputs become admitted jobs.", + "first_step": "Use the exact physical inverse equations in PROOF.md to emit one chronological caller, then price every endpoint and paid operation.", + "blocked_by": "No complete profitable caller, compiler/precision ledger or outer admission is supplied." + } + ], + "checkpoint": { + "canonical_main": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "priority_revision": 7, + "selected_kappa": "0.0030217758", + "frozen_source_payload_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "overlap": [ + "Ali Romman PR5383 retained-center candidate at 4bd6efa51a495a7c7b7754915cf0244e7e60969e", + "Cinna Davis PR4694 retained-center and PR4698 common-chart helper basis", + "Dugongue PR4929 center-free code and coded-native-caller physical normalizers", + "PR5397 scoped owned-exchange ceiling, PR5398 direct backward conjugation and independent PR5399/5400 reviews; these do not supply this unrestricted coupled-output contract." + ], + "campaign_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930", + "frontier_changed": false, + "checked_at_utc": "2026-10-23T22:26:00Z" + } +} diff --git a/research/native-coupled-inverse/VALIDATION.md b/research/native-coupled-inverse/VALIDATION.md new file mode 100644 index 0000000000..8eeb8158f5 --- /dev/null +++ b/research/native-coupled-inverse/VALIDATION.md @@ -0,0 +1,28 @@ +# Validation record + +Canonical source base: `1ec1119972c9aefe42525172d07b332fcff81cb4`. +Pending provider: PR5402 at `3348fccea855082786d5f0fc5558b73d4974e745`. +Environment: CPython 3.12.13, macOS arm64, standard library only. + +The author replay passed the frozen provider's 641-column and 1,240 physical +binding checks. The new verifier passed both full inverse compositions on +632 original columns, all owned-zero checks, unchanged paid counts, the +separate inverse endpoint formula, 464 boundary adjoints, inverse child +phases for ranks 1 through 9, and three semantic rejection controls. + +The registered normal and isolated optimized Python 3.12 replays passed. +All eight archived source files also matched their exact Git blobs at the +pinned PR5402 head. Committed-byte comparison and official export integrity passed for all +16 package and declared-input files at scientific commit +`c85cc03c69137fc198261403b6b674f0e025cf89`. A fresh read-only Git-free export passed the isolated optimized replay. +Hosted CI is separate. + +The optional `--check-source-history` command stopped at its full-history +guard because this checkout is shallow. It did not run its ancestry audit. +The package base is the exact parent of the scientific commit; the eight +archived pending-source files were compared directly with their pinned Git +blobs. These checks do not replace the unrun full-history command. + +No complete caller, full multiplier, selected cold replay, full recursive +compiler or outer admission, independent human review, or formal proof-kernel +check was run. This package gives no new kappa. diff --git a/research/native-coupled-inverse/VERIFY.json b/research/native-coupled-inverse/VERIFY.json new file mode 100644 index 0000000000..71d3718333 --- /dev/null +++ b/research/native-coupled-inverse/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-native-caller/NORMALIZERS.json", + "research/coded-native-caller/PHYSICAL.md", + "research/coded-native-caller/clifford_exact.py", + "research/native-center-free-code/CODE.json", + "research/native-center-free-code/CODED-PROOF.md", + "research/native-center-free-code/SOURCE-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Pinned source replay, exact two-sided inverse on all 632 columns, owned cleanup, unchanged paid profile, inverse child phases and semantic rejection controls." + } + ] +} diff --git a/research/native-coupled-inverse/verify.py b/research/native-coupled-inverse/verify.py new file mode 100644 index 0000000000..8ffb2870da --- /dev/null +++ b/research/native-coupled-inverse/verify.py @@ -0,0 +1,415 @@ +#!/usr/bin/env python3 +"""Verify the native inverse from authenticated source bytes. Apache-2.0.""" + +from pathlib import Path +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +import argparse +import gzip +import importlib.util +import json +import tempfile +import zipfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def check(SRC): + spec = importlib.util.spec_from_file_location("coupled_source", SRC / "verify.py") + s = importlib.util.module_from_spec(spec) + spec.loader.exec_module(s) + s.main() + source = json.loads( + gzip.decompress( + (SRC.parent / "native-center-free-code/SOURCE-WORD.json.gz").read_bytes() + ) + ) + c = source["canonical"] + p = json.loads((SRC / "PROVIDER.json").read_text()) + word = json.loads(gzip.decompress((SRC / "WORD.json.gz").read_bytes()))["word"] + inherited_records = dict(Counter(e[0] for e in word)) + # C0 has no paid call in the changed word. Each live use is a copy of C1..C8. + new = [] + active = None + removed = Counter() + substitutions = [] + for i, e in enumerate(word): + if e[0] == "scalar": + op = e[1] + dst = s.addr(op[1]) + if dst == 632: + if op[0] == "copy": + active = op[2] + else: + active = None + removed[op[0]] += 1 + continue + if op[0] in ("add", "copy") and s.addr(op[2]) == 632: + if active is None: + raise ValueError("C0 read has no retained cache") + e = ["scalar", [op[0], op[1], active, *op[3:]], e[2]] + substitutions.append([i, active]) + new.append(e) + if len(substitutions) != 8: + raise ValueError("expected eight live cache uses") + # Replaying with an initial dirty C0 clear permits the exact source interpreter. + fwd = s.replay([["scalar", ["clear", ["C", 0]], 0]] + new, c, 641) + old = s.replay(word, c, 641) + if ( + fwd[0] != old[0] + or fwd[1][:632] + fwd[1][633:] != old[1][:632] + old[1][633:] + or fwd[2] != old[2] + ): + raise ValueError("dead accumulator elimination changed endpoint") + + def identity(): + return [{(j, ()): F(1)} for j in range(641)] + + def linear(ops, rows): + for e in ops: + if e[0] == "add": + s.add(rows[e[1]], rows[e[2]], F(e[3])) + else: + rows[e[1]] = {k: v * F(e[2]) for k, v in rows[e[1]].items()} + + # Apply a native word to supplied columns, with exact inverse child frames. + def apply(program, rows, charts, reverse=False, copy_sign=-1): + paid = Counter() + clears = [] + copies = [] + for index, e in ( + reversed(list(enumerate(program))) if reverse else enumerate(program) + ): + kind = e[0] + if kind == "scalar": + op, frame = e[1:] + dst = s.addr(op[1]) + if op[0] == "clear": + if reverse: + if rows[dst]: + raise ValueError("reverse initial clear is not zero") + clears.append(dst) + else: + rows[dst] = {} + charts[dst] = frame + elif op[0] == "copy": + src = s.addr(op[2]) + if charts[src] != frame or charts[dst] != frame: + raise ValueError("copy charts") + if reverse: + s.add(rows[dst], rows[src], copy_sign) + if rows[dst]: + raise ValueError("inverse copy did not erase cache") + copies.append(dst) + else: + if rows[dst]: + raise ValueError("copy input not zero") + rows[dst] = dict(rows[src]) + elif op[0] == "add": + src = s.addr(op[2]) + if charts[src] != frame or charts[dst] != frame: + raise ValueError("add charts") + s.add( + rows[dst], rows[src], F(op[3], op[4]) * (-1 if reverse else 1) + ) + else: + if charts[dst] != frame: + raise ValueError("scale chart") + a = F(op[2], op[3]) + a = 1 / a if reverse else a + rows[dst] = {k: v * a for k, v in rows[dst].items()} + elif kind == "warp": + _, ref, w, a, b = e + dst = s.addr(ref) + if reverse: + w = -w + a, b = b, a + if charts[dst] != a: + raise ValueError("warp chart") + sym = (1 if w > 0 else -1) * (abs(w) + 1000000) + out = {} + for (owner, t), v in rows[dst].items(): + t = t[1:] if t and t[0] == -sym else (sym,) + t + s.add(out, {(owner, t): v}) + rows[dst] = out + charts[dst] = b + elif kind == "climb": + _, _, dst, a, b, r = e + if reverse: + a, b = b, a + if ( + charts[dst] != a + or abs(len(c["frames"][a]) - len(c["frames"][b])) != r + ): + raise ValueError("child chart") + charts[dst] = b + paid[r] += 1 + elif kind == "zero_retag": + _, dst, a, b = e + if reverse: + a, b = b, a + if charts[dst] != a or rows[dst]: + raise ValueError("nonzero retag") + charts[dst] = b + elif kind not in ("phase", "adapter", "residual_adapter"): + raise ValueError(kind) + return paid, clears, copies + + w = json.loads((SRC / "WITNESS.json").read_text()) + records = p["mode_boundaries"] + perm = p["candidate_mode_permutation"] + sign = list(map(F, p["candidate_mode_signs"])) + factors = { + r["cache_slot"]: F(w[r["witness_row"]]["zero_factor"]) * sign[r["witness_row"]] + for r in records + } + + def full(rows, reverse=False, copy_sign=-1): + # Logical normalization: physical monomial boundaries are inverted separately. + for j in range(632, 641) if reverse else [632]: + rows[j] = {} + if not reverse: + charts = c["start"][:] + [None] * 9 + linear(p["input_basis_program"], rows) + stats = apply(new, rows, charts) + linear(p["output_basis_program"], rows) + for r in records: + a, b = r["owner"], r["cache_slot"] + f = factors[b] + rows[b] = {k: v / f for k, v in rows[b].items()} + if rows[a]: + raise ValueError("forward swap owner nonzero") + rows[a], rows[b] = rows[b], rows[a] + else: + charts = c["final"][:] + [None] * 9 + for r in records: + a, b = r["owner"], r["cache_slot"] + f = factors[b] + rows[a], rows[b] = rows[b], rows[a] + rows[b] = {k: v * f for k, v in rows[b].items()} + charts[b] = r["frame"] + linear(p["input_basis_program"], rows) + stats = apply(new, rows, charts, True, copy_sign) + linear(p["output_basis_program"], rows) + if any(rows[632:]): + raise ValueError("owned output nonzero") + # Clear the eight owned cache returns after the exact zero check. + for owner in range(633, 641): + rows[owner] = {} + return rows, stats + + f, fs = full(identity()) + b, bs = full(identity(), True) + if fs[0] != bs[0] or bs[0] != Counter({int(k): v for k, v in p["paid"].items()}): + raise ValueError("paid mismatch") + for first, back in ((f, True), (b, False)): + z, _ = full([dict(r) for r in first], back) + if z[:632] != identity()[:632] or any(z[632:]): + raise ValueError("not a two-sided inverse") + # Check the inverse independently from the full scalar endpoint formula. + M = json.loads((SRC.parent / "coded-native-caller/NORMALIZERS.json").read_text())[ + "mode_columns" + ] + for j in range(632): + row = {(j, ()): F(1)} + if j < 112: + row[(112 + j, ())] = F(1) + for k in range(8): + s.add(row, {(p["mode_owners"][k], ()): F(1)}, -F(M[k][j], 4)) + for i in range(112): + s.add(row, {(112 + i, ()): F(1)}, -F(M[k][j] * M[k][i], 4)) + if j in p["mode_owners"]: + k = p["mode_owners"].index(j) + for i in range(112): + s.add(row, {(112 + i, ()): F(1)}, M[k][i]) + row = {k: v for k, v in row.items() if v} + if b[j] != row: + raise ValueError("independent inverse formula") + controls = [] + try: + full(identity(), True, 1) + except ValueError as exc: + if str(exc) != "inverse copy did not erase cache": + raise + controls.append("wrong inverse COPY sign rejected") + if len(controls) != 1: + raise ValueError("wrong COPY sign accepted") + try: + apply( + [["zero_retag", 0, c["start"][0], c["start"][0]]], + identity(), + c["start"][:] + [None] * 9, + True, + ) + except ValueError as exc: + if str(exc) != "nonzero retag": + raise + controls.append("nonzero reverse retag rejected") + if len(controls) != 2: + raise ValueError("nonzero retag accepted") + # Each inverse rank-r Gaussian is the positive child followed by a bit translation. + _, _, ce = s.authenticate() + for rank in range(1, 10): + G = ce.fourier(9, range(rank)) + positive = G.then(ce.xgate(9, (1 << rank) - 1)) + inverse = G.adjoint() + if positive.tab != inverse.tab or positive.zero_state() != inverse.zero_state(): + raise ValueError("inverse child phase") + # Exact adjoints of each physical boundary retain their absolute phases. + normal = json.loads( + (SRC.parent / "coded-native-caller/NORMALIZERS.json").read_text() + ) + words = [r[k]["literal_word"] for r in records for k in ("input_K", "output_N")] + words += [ + port["compiled_wrappers"][k]["word"] + for port in normal["ports"] + for k in ( + "backward_input_X", + "backward_input_Y", + "backward_output_X", + "backward_output_Y", + ) + ] + + def literal(word): + op = ce.ident(9) + for e in word: + if e[0] == "P": + a = ce.perm(9, tuple(e[1])) + elif e[0] == "D": + a = ce.diag(9, tuple(e[1]), tuple(e[2])) + elif e[0] == "X": + a = ce.xgate(9, e[1]) + elif e[0] == "phase": + a = ce.Op(9, ce.identity(9), [("phase", e[1])]) + else: + raise ValueError("nonmonomial wrapper") + op = op.then(a) + return op + + for word in words: + A = literal(word) + B = literal(A.adjoint().circuit) + for v in (A.then(B), B.then(A)): + if v.tab != ce.identity(9) or v.zero_state() != ce.ident(9).zero_state(): + raise ValueError("boundary inverse phase") + bad = literal(words[0]).adjoint() + bad = ce.Op(9, bad.tab, bad.circuit + [("phase", 1)]) + v = literal(words[0]).then(bad) + if v.zero_state() == ce.ident(9).zero_state(): + raise ValueError("phase mutation accepted") + controls.append("same-tableau inverse phase error rejected") + # Count the literal schedule, including inverse cache ADDs and initialization. + ordinary_forward = Counter(e[1][0] for e in new if e[0] == "scalar") + ordinary_inverse = Counter() + for e in new: + if e[0] == "scalar" and e[1][0] != "clear": + ordinary_inverse["add" if e[1][0] == "copy" else e[1][0]] += 1 + for program in (p["input_basis_program"], p["output_basis_program"]): + for e in program: + ordinary_forward[e[0]] += 1 + ordinary_inverse[e[0]] += 1 + ordinary_forward.update(clear=9, scale=16, swap=8, monomial=464) + ordinary_inverse.update(clear=17, scale=16, swap=8, monomial=464) + # A positive-child inverse needs at most one further translation per paid call. + ordinary_inverse["child_inverse_translation"] += sum(bs[0].values()) + + def log_bound(a): + e = 0 + while a > 1: + a /= 2 + e += 1 + return e + + bound = 0 + for e in new: + if e[0] == "scalar": + op = e[1] + if op[0] == "add": + bound += log_bound(1 + abs(F(op[3], op[4]))) + elif op[0] == "copy": + bound += 1 + elif op[0] == "scale": + bound += log_bound(max(F(1), abs(F(op[3], op[2])))) + for program in (p["input_basis_program"], p["output_basis_program"]): + for e in program: + bound += ( + log_bound(1 + abs(F(e[3]))) + if e[0] == "add" + else log_bound(max(F(1), abs(F(e[2])))) + ) + bound += sum(log_bound(max(F(1), abs(1 / F(r["cache_scalar"])))) for r in records) + receipt = { + "status": "PASS_SAME_PAID_NATIVE_TWO_SIDED_INVERSE", + "source_pr": 5402, + "source_head": "3348fccea855082786d5f0fc5558b73d4974e745", + "independent_original_columns": 632, + "owned_outputs_zero": 9, + "paid": dict(sorted(bs[0].items())), + "removed_dead_C0_records": dict(removed), + "live_cache_substitutions": substitutions, + "inverse_copy_uncomputations": bs[2], + "inherited_record_types": inherited_records, + "boundary_adjoint_checks": len(words), + "inverse_child_ranks_checked": list(range(1, 10)), + "ordinary_forward": dict(ordinary_forward), + "ordinary_inverse": dict(ordinary_inverse), + "inverse_local_amplification_power2_bound": bound, + "failure_controls": controls, + "scope": "All-width native inverse of the coupled provider; no autonomous credit for the coupled outputs, complete caller, full precision/compiler bill or new kappa.", + } + return receipt + + +def main(emit=False): + origins = json.loads((HERE / "ORIGINS.json").read_text()) + pins = json.loads((HERE / "SOURCES.json").read_text()) + archive = (HERE / "SOURCE.zip").read_bytes() + if sha256(archive).hexdigest() != origins["archive_sha256"]: + raise ValueError("source archive changed") + with tempfile.TemporaryDirectory(prefix="native-coupled-inverse-") as tmp: + root = Path(tmp) + src = root / "research/native-rank8-helper-provider" + src.mkdir(parents=True) + with zipfile.ZipFile(HERE / "SOURCE.zip") as z: + if set(z.namelist()) != {r["file"] for r in origins["files"]}: + raise ValueError("source archive inventory") + for row in origins["files"]: + data = z.read(row["file"]) + if sha256(data).hexdigest() != row["sha256"]: + raise ValueError("source archive member changed") + (src / row["file"]).write_bytes(data) + for row in pins["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + if sha256(data).hexdigest() != row["sha256"]: + raise ValueError("main input changed") + dst = root / row["path"] + dst.parent.mkdir(parents=True, exist_ok=True) + dst.write_bytes(data) + receipt = check(src) + receipt = json.loads(json.dumps(receipt)) + if emit: + (HERE / "RESULT.json").write_text(json.dumps(receipt, indent=2) + "\n") + elif receipt != json.loads((HERE / "RESULT.json").read_text()): + raise ValueError("committed receipt differs") + print( + receipt["status"], + json.dumps( + { + "columns": 632, + "owned_zero": 9, + "paid": receipt["paid"], + "controls": len(receipt["failure_controls"]), + } + ), + ) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + main(parser.parse_args().emit)