From a3b9733472db1da15d93745e9859b6a11bc1a555 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 23:44:28 -0700 Subject: [PATCH] research: expose coded reverse physical pair substitution gap --- .../coded-reverse-physical-pair-gap/README.md | 93 +++++++ .../RESULT.json | 92 +++++++ .../SOURCES.json | 72 +++++ .../coded-reverse-physical-pair-gap/TASK.json | 94 +++++++ .../VALIDATION.md | 18 ++ .../VERIFY.json | 40 +++ .../coded-reverse-physical-pair-gap/verify.py | 253 ++++++++++++++++++ 7 files changed, 662 insertions(+) create mode 100644 research/coded-reverse-physical-pair-gap/README.md create mode 100644 research/coded-reverse-physical-pair-gap/RESULT.json create mode 100644 research/coded-reverse-physical-pair-gap/SOURCES.json create mode 100644 research/coded-reverse-physical-pair-gap/TASK.json create mode 100644 research/coded-reverse-physical-pair-gap/VALIDATION.md create mode 100644 research/coded-reverse-physical-pair-gap/VERIFY.json create mode 100644 research/coded-reverse-physical-pair-gap/verify.py diff --git a/research/coded-reverse-physical-pair-gap/README.md b/research/coded-reverse-physical-pair-gap/README.md new file mode 100644 index 0000000000..fe31036c0e --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/README.md @@ -0,0 +1,93 @@ +# The first physical substitution gap in the coded reverse controller + +**Scoped counterexample and missing implication. No complete caller obstruction or new κ is claimed.** Under the signed physical normalizers of Dillon's PR4933, the literal PR4940 backward FULL followed by its scalar `A^-1` thin source leaves the nonzero block `D(I-A^-1 C)`. The declared x-only input/output recodings do not remove this block. A common full exit frame allows scalar owner mixing; it does not identify the physical code `C` with scalar `A`. + +## Source and chronological cut + +The canonical base is `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority revision 7. [SOURCES.json](SOURCES.json) authenticates every external live input. The PR4933 head `d969c458c24278e0fd37e5b4c0ff8a53a496b430` and PR4929 head `361f5d4100640177d6a983dd2f336021c75bfd5e` are ancestors of that base; the used `NORMALIZERS.json`, `PHYSICAL.md`, and PR4929 `CODE.json` match their original head bytes. No unmerged shared-object dependency or frozen-source edit is introduced. + +The exact PR4940 source is `research/coded-reverse-controller/verify.py`: `local()` applies a backward shear, then its `D_s`; `build()` binds `Qv=2` and every `D_s` to scalar numbers. This proves a commuting specialization, rather than the physical noncommuting substitution. For the proposed `p=19` word choose its final backward stage 37 and its next forward thin stage 38. `j < p-1` and the initial-IDLE condition are both false here, so no bridge or IDLE lies between these calls. Terminal IDLEs on other pairs occur after this thin shear. The test uses the central address bit and stage 37's fresh eight bits; every other address block is retained as a spectator. + +This package checks the local operator identity required by the proposed conjugation. It does not infer that a later whole-controller continuation cannot cancel a local discrepancy. Such a continuation would require a different, explicit source-bound proof and bill. + +## Exact local calculation + +Operators apply rightmost first. Let `Q` be the actual central Gaussian, `D` the eight fresh-axis Gaussian product, and `R=DQ`. PR4933 supplies signed monomial `K_i`, with `[K_i,R]=0`, and the physical code + +```text +C_ij = A_ij K_i^-1 K_j, C = K^-1 (A tensor I) K, +B = diag(D,D) [[I,-Q C],[0,I]]. +``` + +Its actual X-only `Q^2` raw-dual convention is retained. We never replace it with the older Y-only convention or assume `[C,Q]=0`. The literal PR4940 thin source is copied into owned fields, mixed by scalar `A^-1`, queried by `Q^-1`, and added to Y. Therefore + +```text +T = [[I,0],[Q^-1 A^-1,I]], +T B = [[D, -D Q C], + [D Q^-1 A^-1, D(I-A^-1 C) ]]. +``` + +Only scalar `A^-1` was commuted with `D` and `Q`. In particular no step commutes `C` past either operator. With the declared boundary `pre X A`, `post X A^-1`, this becomes + +```text +[[D, -D Q A^-1 C], + [D Q^-1, D(I-A^-1 C)]]. +``` + +The standard pair is `[[D,-DQ],[D Q^-1,0]]`. Thus this local binding holds **if and only if `C=A tensor I`**. The source polynomial `A^2+12A=13I` establishes invertibility and its scalar inverse; it does not establish that missing operator equality. + +## Literal signed witness + +Use destination owner 0, source owner 1, and source address `1`. The actual ports are `q_0=11`, `q_1=19`; their normalizer masks are `z_0=15`, `z_1=23`. The pinned scalar entry is `A_01=-1/2`. Their exact signed actions give + +```text +K_1 |1> = -|19>, K_0^-1 |19> = |22>, +C_01 |1> = +|22>/2, (A tensor I)_01 |1> = -|1>/2. +``` + +For the arbitrary local input `x=0`, `y=|owner 1,address 1>`, the residual is `y_out=D(I-A^-1 C)y`. Applying the invertible diagnostic `A D^-1` gives, at owner 0, `-(|1>+|22>)/2`, proving that the actual output is nonzero. The diagnostic is a mathematical witness, **not an emitted decoder or free physical operation**. Because `D` is a product of invertible actual Gaussian gates, multiplying by `D` cannot erase this discrepancy. Pre/post operations restricted to X do not affect the displayed Y-to-Y block. + +This failure holds at every positive digit-column width: use `|1>` in one column and `|0>` in the others. Each `K_i,f` is the source signed tensor lift, so its transition still distinguishes the same two addresses, while scalar `A_01` is applied once to the owner block. The proof evaluates the finite owner program in the lifted operator algebra; it does not tensor a sum or replace owner code `A` by `A^tensor f`. + +## Complete local operation ledger + +The ledger prices the **failed literal recipe**, with the two declared boundary recodings charged once. In a complete controller those two conversions belong to its boundary, rather than every adjacent pair. No favorable moment is inferred from this local invoice. + +| Operation | Field-level charge | Status | +|---|---:|---| +| Backward center-free FULL | `2201 H1 + 412 H2 + 510 H3 + 127 H4 + 40 H5` | Inherited PR4929 paid profile, unchanged | +| Original helper returns | `28 H4 + 7 H7 + 47 H8 + 326 H9` on 408 distinct owners | Inherited autonomous jobs, no scratch or erasure credit | +| Four native port wrappers | 448 monomial field maps | Retained PR4933 upper bound | +| X-only backward conversion | At most 448 more monomial field maps | Retained bound; no fusion assumed | +| Input `A`, thin-source `A^-1`, output `A^-1` | Three eight-mode recodings: 2,688 scalar ADDs and 48 owned CLEARs | Constructive source program; eight reusable owned mode fields | +| Thin source bank | 112 initial CLEARs, 112 COPYs, 112 terminal owned ERASEs | 112 simultaneously owned fields, separate from helpers | +| Thin queries | 112 rank-one Gaussian jobs and 112 Pauli translations for `Q^-1` | Positive Gaussian lowering from PR4440; inverse is not order two | +| Thin destination updates | 112 ADDs | Main inputs are arbitrary and distinct | + +The resulting paid Gaussian profile is `{1:2313,2:412,3:510,4:127,5:40}`; the wrapper/query count is at most 1,008 monomial field maps, in addition to the native word's internal work. The added recoding/query workspace peaks at 120 owned fields (112 query copies plus eight modes), beyond inherited native scratch. Each recoding completes every mode source read before updating its owner bank. Its owned temporaries alone are cleared, and no original helper is modified by the new word. + +Scalar `A` uses update coefficient `-1/4`; each scalar inverse uses `-1/52`, introducing denominator 13 twice in this local boundary-inclusive recipe. Native ordinary arithmetic, its 6,596 dyadic compensation ADDs, matcher/routing work, complete fixed-tape field-map tariffs, rounding and denominator-13 implementation remain inherited or unresolved **nonzero costs**. Their absence from a concrete TM tariff is a limitation, not free credit. Task 03 independently addresses the local odd-division kernel; it cannot make `C=A tensor I` true. No independent Gaussian main-output credit is admitted for this failed recipe. + +The nearby alternative `Q^-1 C^-1` thin source is not silently excluded: `[C,DQ]=0` makes that alternative's Y-to-Y block zero. It is a changed recipe costing an additional 224 `K_i/K_i^-1` field maps per inverse recoding, and its other blocks and actual boundary still need proof. This package stops at the literal scalar-substitution gap instead of claiming a general impossibility. + +## Reproduce and evidence + +```sh +python3.12 -I -B research/coded-reverse-physical-pair-gap/verify.py +python3.12 -I -O -B research/coded-reverse-physical-pair-gap/verify.py +python3.12 -B scripts/research_package.py --package research/coded-reverse-physical-pair-gap +``` + +The verifier uses only the standard library. It authenticates the source bytes, checks all 112 signed normalizers and their exact absolute-phase weight identities, and checks all 12,544 owner-code entries against the eight-mode program. An independent address-array oracle over `F_65537`, with `i=256`, executes the actual `Q` and all eight `D` axes on the 112-owner fixture. Denominators 2 and 13 are invertible in this field, so its nonzero residual also rejects exact rational operator equality. The exact sparse witness supplies the literal rational discrepancy separately. + +The scalar-A predecessor is a positive cancellation control. Omitting the `K` sign changes the exact witness; commuting `C` through `Q` or copying the Y-only backward convention changes the operator. The new cleanup trace permits only the 120 owned fields and rejects an attempted ERASE of arbitrary helper 17. This verifies the new wrapper's ownership declaration, while original producer autonomy remains an explicit inherited source premise. [RESULT.json](RESULT.json) records the mathematical receipt. No original three-minute replay, full p19 controller, Lean, production build, compiler, hosted CI, or multiplication theorem was run. + +## Open next questions + +The structured question in [TASK.json](TASK.json) is a changed thin/boundary word that proves **every** block of the physical pair and its complete added bill. The first useful check is the same signed owner-0/owner-1 fixture, followed by an all-input typed operator derivation. A product of changed stage codes or a paid boundary can evade this local gap; neither is furnished here. A denominator kernel is a separate conditional arithmetic result, rather than a physical consumer proof. + +## Credit and scope change + +This changes the `centre-path-sharing` card to PR4940's explicitly handed-off physical-pair obligation. It does not re-prove PR4933's normalizers, its local gauges, or its one-stage terminal support theorem, and it does not repeat PR4932's standalone one-bank exclusion. The new result is the exact first mismatch in PR4940's scalar-to-physical substitution, its source-bound signed witness, and the boundary-inclusive local ledger. + +Credit Cayden Burkart / SethBurkart123 for PR4940's coded reverse controller; Dillon for PR4933's signed physical normalizers, eight-mode scalar program and X-only backward convention; Dugongue / mdumitrean for PR4929's coded producer; Cinna Davis for PR4694/4698 and PR4440/4470; Cao Yifan / intqwq for PR4610; zxv, Jacob Alan Sussman, and every retained native, Clifford, query, ownership, compiler and precision contributor. Prepared for JoyboyBrian with substantial OpenAI Codex assistance. New work is Apache-2.0. Independent human or formal-kernel acceptance is not claimed. diff --git a/research/coded-reverse-physical-pair-gap/RESULT.json b/research/coded-reverse-physical-pair-gap/RESULT.json new file mode 100644 index 0000000000..09bbab14d3 --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/RESULT.json @@ -0,0 +1,92 @@ +{ + "addresses_per_owner": 512, + "all_width_argument": "Evaluate each signed K tensor lift inside each owner block; A is applied once. C_f != A tensor I at every f>=1 and D_f is invertible.", + "chronological_cut": { + "backward_stage": 37, + "intervening_bridge_or_idle": false, + "next_thin_stage": 38, + "p": 19 + }, + "controls": [ + "scalar-A predecessor cancels", + "omitted K sign changes witness", + "C-Q commutation fails", + "Y-only backward convention fails", + "arbitrary helper erasure rejected" + ], + "exact_witness": { + "A_01": "-1/2", + "A_01_output": { + "1": "-1/2" + }, + "C_01_output": { + "22": "1/2" + }, + "destination_port": 0, + "diagnostic_A_Dinv_y": { + "1": "-1/2", + "22": "-1/2" + }, + "input_address": 1, + "source_port": 1 + }, + "independent_helper_owners": 408, + "local_invoice": { + "denominators": [ + 4, + 52 + ], + "native_helper_profile_retained": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "native_wrapper_maps_upper": 896, + "new_recursive_jobs_beyond_native": { + "1": 112 + }, + "owned_query_copies": 112, + "owned_query_erasures": 112, + "owned_query_initial_clears": 112, + "owned_recoding_clears": 48, + "paid_gaussian_profile": { + "1": 2313, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "peak_added_owned_fields": 120, + "query_destination_adds": 112, + "recoding_adds": 2688, + "scalar_A_or_Ainv_evaluations": 3, + "thin_inverse_query_pauli_maps": 112, + "unknown_not_zero": [ + "inherited native ordinary work", + "fixed-tape matching/routing and field-map tariff", + "odd-denominator precision and rounding", + "whole-controller productive endpoint and compiler" + ] + }, + "modular_oracle": { + "actual_D_axes": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "i": 256, + "nonzero_residual_coordinates": 25324, + "prime": 65537 + }, + "owners": 112, + "pair_y_to_y_block": "D*(I-A^-1*C)", + "scope": "First literal PR4940 pair under the signed PR4933 physical binding; no general caller obstruction", + "status": "PASS_CODED_REVERSE_PHYSICAL_PAIR_GAP", + "width": 1 +} diff --git a/research/coded-reverse-physical-pair-gap/SOURCES.json b/research/coded-reverse-physical-pair-gap/SOURCES.json new file mode 100644 index 0000000000..a3f9e3d6e5 --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coded-native-caller/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "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/native-source.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/coded-reverse-controller/README.md", + "usage": "input", + "git_blob": "998410d16e16fefc6de982edfd1496f315146a4a", + "sha256": "f7bb9a2ba49cf7efa87fd68cc2d095e0ddff458f1360e504a2b16cf5caaa8d46" + }, + { + "path": "research/coded-reverse-controller/TASK.json", + "usage": "input", + "git_blob": "1e2a46f85ea129be1d5f78ed7c70f4dd3ac2b856", + "sha256": "da8a45d60c219d0dee9de8b1133f93231257d4ed0afce6399eee49b3c4f6e583" + }, + { + "path": "research/coded-reverse-controller/verify.py", + "usage": "input", + "git_blob": "71f3d8929f28d7b4b854be7177ca8dfecf81ea5c", + "sha256": "05a898d3af329dc4665590b4ec4b2801e588843efe9618eec55b4028fd104b67" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/native-center-free-code/README.md", + "usage": "input", + "git_blob": "26144655f8c05842e42ed5c5a1ca726a09c1ac69", + "sha256": "fede7462b9f0048f8c8a8756bd2bdac6389448c2fbfa12541a564d1088198cad" + } + ] +} diff --git a/research/coded-reverse-physical-pair-gap/TASK.json b/research/coded-reverse-physical-pair-gap/TASK.json new file mode 100644 index 0000000000..473a766a07 --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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": "Source-bound first backward FULL / next A^-1-mixed thin shear / x-only input-output boundary. Locate the first failed physical substitution using all 112 signed owner normalizers; no full controller replay.", + "scope_change_reason": "PR4940 formally treats its code A as scalar in the physical Q,D representation. PR4933 realizes C_ij=A_ij K_i^-1 K_j. Test this exact binding rather than the old center-sharing question or another formal root.", + "bottleneck_link": "The removed eight rank-eight centers do not establish a usable supplier until the actual thin consumer and its boundary implement the claimed uncoded endpoint.", + "budget_minutes": 60, + "stop_rule": "Stop at one exact local pair or the first decisive failed substitution. No full p16 replay, new code family, compiler admission, or kappa claim.", + "outcome": "negative-result", + "evidence": "Exact signed block C01|1>=+|22>/2 differs from A01|1>=-|1>/2. The direct modular physical pair including Q and all eight D axes leaves D(I-A^-1 C)y nonzero. Both declared x-only boundaries preserve that y block.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for source binding, derivation, verifier, and documentation.", + "open_questions": [ + { + "question": "Which changed thin and boundary word realizes the full uncoded local pair with PR4933 physical C?", + "why_it_matters": "The literal scalar A^-1 substitution leaves a nonzero y-to-y block, so the formal controller invoice is not physically bound.", + "first_step": "Bind a proposed replacement to the same B=D U(-Q C) and test both diagonal and off-diagonal blocks with its complete extra bill.", + "blocked_by": "No such complete replacement word is supplied here." + } + ], + "first_fixture": { + "width": 1, + "owners": 112, + "backward_stage": 37, + "next_thin_stage": 38, + "input": "x=0, y owner 1 at address 1; all 408 helper owners arbitrary and independent", + "witness_block": [ + 0, + 1 + ], + "expected_gap": "D*(I-A^-1*C)*y != 0 even after the declared x-only A/A^-1 boundary", + "p": 19 + }, + "bounds": { + "address_bits": 9, + "address_count": 512, + "modulus": 65537, + "max_local_check_seconds": 10, + "recoding_scratch_owners": 8 + }, + "success_condition": "Emit the exact failed block A01=-1/2, K0^-1 K1|1>=-|22> and verify that the actual pair leaves a nonzero y response; count every retained local operation and explicit unknown.", + "inherited_obligations": [ + "PR4929 arbitrary-input producer and 408 autonomous helper jobs", + "PR4933 signed physical central ABI and retained native normalizers", + "PR4440 all-column query job, owned-stream erasure, matching and routing", + "Odd-denominator arithmetic, precision/tape/compiler admission remain open" + ] +} diff --git a/research/coded-reverse-physical-pair-gap/VALIDATION.md b/research/coded-reverse-physical-pair-gap/VALIDATION.md new file mode 100644 index 0000000000..561151c248 --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/VALIDATION.md @@ -0,0 +1,18 @@ +# Validation and exact scope + +Local environment: macOS, CPython 3.12. All scientific commands ran sequentially under the batch's global `serial.py` lock. No original native verifier or controller replay was launched. + +| Command | Result | +|---|---| +| `python3.12 -I -B research/coded-reverse-physical-pair-gap/verify.py --write` | PASS; first measured scientific run 0.57 seconds, then a final authoring replay passed below one second | +| `python3.12 -B scripts/research_package.py --package research/coded-reverse-physical-pair-gap` | PASS_REGISTERED_RESEARCH_PACKAGE, including normal and `-O` direct commands | + +The first timing wrapper used `/usr/bin/time -l`; the verifier passed, but macOS denied that wrapper's optional `sysctl kern.clockrate` statistic. Its nonzero wrapper exit is not reported as a successful complete command. The later direct and registered commands exit successfully without that statistic. + +The exact sparse signed witness, positive scalar-A fixture, phase and noncommutation controls, actual 112-owner modular pair with all eight fresh Gaussian axes, and owned-only cleanup control all pass. The receipt reports the residual's actual nonzero coordinate count. The normal/optimized replay uses explicit exceptions, so none of its correctness checks disappears under `-O`. + +The added verifier's authoring gate is: (1) it protects the observable physical pair equality required by PR4940's proposed scalar-code substitution; (2) replacing physical `C` by scalar `A`, omitting the signed normalizer, commuting `C` through `Q`, or clearing an original helper is the credible failure; (3) PR4940's existing binding specializes `Q,D` to scalars and PR4933's normalizer/gauge checks do not test this literal next thin source and its x-only boundary; (4) no production export, test hook, shared-code change, or existing test modification is needed. + +The source-head byte and ancestry checks confirm that PR4933 head `d969c458c24278e0fd37e5b4c0ff8a53a496b430` and PR4929 head `361f5d4100640177d6a983dd2f336021c75bfd5e` are ancestors of the canonical base and that the used mathematical source bytes match. The package's declared Git provenance itself resolves through the pinned canonical base, so no pending foreign object is required for replay. + +Material limitations: the producer's all-input identity and autonomous helper transforms are inherited source premises; new wrappers use the pinned signed physical ABI. This is a local scalar-substitution gap, not a rejection of every noncommuting caller or the full PR4940 endpoint. Fixed-point odd division, complete native ordinary work, tape routing, compiler, full-controller cancellation, hosted CI and formal-kernel acceptance remain unrun or unresolved. No multiplication exponent or selected record changes. diff --git a/research/coded-reverse-physical-pair-gap/VERIFY.json b/research/coded-reverse-physical-pair-gap/VERIFY.json new file mode 100644 index 0000000000..ca7fcd8ffd --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-native-caller/CODE.json", + "research/coded-native-caller/NORMALIZERS.json", + "research/coded-native-caller/PHYSICAL.md", + "research/coded-native-caller/native-source.json.gz", + "research/coded-reverse-controller/README.md", + "research/coded-reverse-controller/TASK.json", + "research/coded-reverse-controller/verify.py", + "research/native-center-free-code/README.md", + "research/query-thinned-controllers/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact signed source block, all-owner modular physical pair, x-only boundary residual, scalar-A positive fixture and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same complete checks with assertions disabled." + } + ] +} diff --git a/research/coded-reverse-physical-pair-gap/verify.py b/research/coded-reverse-physical-pair-gap/verify.py new file mode 100644 index 0000000000..bad39406c4 --- /dev/null +++ b/research/coded-reverse-physical-pair-gap/verify.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""First physical PR4940 pair, independently evaluated with signed PR4933 K. + +Apache-2.0. Prepared for JoyboyBrian with substantial OpenAI Codex assistance. +Source authors and inherited proof obligations are credited in README.md. +""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import argparse +import gzip +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +P = 65537 +IMAG = 256 +OWNERS = 112 +SIZE = 512 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def parity(x): + return x.bit_count() & 1 + + +def mv(rows, x): + return sum(parity(row & x) << bit for bit, row in enumerate(rows)) + + +def transpose(rows): + return [sum(((row >> bit) & 1) << j for j, row in enumerate(rows)) + for bit in range(9)] + + +def signed_map(record, x, inverse=False, unsigned=False): + rows, mask = record["G_rows"], record["Z_mask"] + y = mv(transpose(rows) if inverse else rows, x) + sign = 1 if unsigned else 1 - 2 * parity(mask & (x if inverse else y)) + return y, sign + + +def block(record_i, record_j, vector, coefficient, unsigned=False): + out = {} + for x, value in vector.items(): + y, sj = signed_map(record_j, x, unsigned=unsigned) + z, si = signed_map(record_i, y, inverse=True, unsigned=unsigned) + out[z] = out.get(z, 0) + coefficient * si * sj * value + return {x: value for x, value in out.items() if value} + + +def sparse_q(vector, inverse=False): + # Gaussian-rational pairs retain absolute phase without complex floats. + s = -1 if inverse else 1 + out = {} + for x, (re, im) in vector.items(): + for y, a, b in ((x, F(1, 2), F(s, 2)), + (x ^ 1, F(1, 2), F(-s, 2))): + old = out.get(y, (F(0), F(0))) + out[y] = (old[0] + a * re - b * im, + old[1] + a * im + b * re) + return {x: value for x, value in out.items() if value != (0, 0)} + + +def sparse_block(ri, rj, vector, coefficient): + out = {} + for component in (0, 1): + values = block(ri, rj, {x: v[component] for x, v in vector.items()}, coefficient) + for x, value in values.items(): + old = list(out.get(x, (F(0), F(0)))) + old[component] = value + out[x] = tuple(old) + return {x: value for x, value in out.items() if value != (0, 0)} + + +def empty(): + return [[0] * SIZE for _ in range(OWNERS)] + + +def add(x, y, sign=1): + return [[(a + sign * b) % P for a, b in zip(xi, yi)] + for xi, yi in zip(x, y)] + + +def gaussian(bank, axes, inverse=False): + a = (1 + (-IMAG if inverse else IMAG)) * pow(2, -1, P) % P + b = (1 - (-IMAG if inverse else IMAG)) * pow(2, -1, P) % P + out = [row[:] for row in bank] + for bit in axes: + step = 1 << bit + for row in out: + for start in range(0, SIZE, 2 * step): + for x in range(start, start + step): + u, v = row[x], row[x + step] + row[x] = (a * u + b * v) % P + row[x + step] = (b * u + a * v) % P + return out + + +def scalar_code(bank, modes, inverse=False): + temp = [[sum(sign * bank[i][x] for i, sign in contacts) % P + for x in range(SIZE)] for contacts in modes] + denominator = pow(52 if inverse else 4, -1, P) + out = [row[:] for row in bank] + for mode, contacts in enumerate(modes): + for i, sign in contacts: + out[i] = [(a - sign * denominator * b) % P + for a, b in zip(out[i], temp[mode])] + return out + + +def physical_code(bank, records, modes): + mixed = empty() + for i, row in enumerate(bank): + for x, value in enumerate(row): + if value: + y, sign = signed_map(records[i], x) + mixed[i][y] = sign * value % P + mixed = scalar_code(mixed, modes) + out = empty() + for i, row in enumerate(mixed): + for x, value in enumerate(row): + if value: + y, sign = signed_map(records[i], x, inverse=True) + out[i][y] = sign * value % P + return out + + +def run(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + need(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "Changed pinned source: " + row["path"]) + source = ROOT / "research/coded-native-caller" + receipt = json.loads((source / "NORMALIZERS.json").read_text()) + records = receipt["ports"] + canonical = json.loads(gzip.decompress((source / "native-source.json.gz").read_bytes()))["canonical"] + A = [[F(value) for value in row] + for row in json.loads((source / "CODE.json").read_text())["A"]] + columns = receipt["mode_columns"] + need(len(records) == len(A) == OWNERS and all(len(row) == OWNERS for row in A), "112 owners") + need(len(columns) == 8, "Eight source modes") + need(all(A[i][j] == F(i == j) - F(sum(c[i] * c[j] for c in columns), 4) + for i in range(OWNERS) for j in range(OWNERS)), "Every scalar code block") + need(all(sum(a * b for a, b in zip(u, v)) == 56 * (j == k) + for j, u in enumerate(columns) for k, v in enumerate(columns)), "Inverse factorization") + for i, record in enumerate(records): + rows, z = record["G_rows"], record["Z_mask"] + need(record["port"] == i and record["q"] == canonical["ports"][i], "Actual owner ports") + need(mv(rows, 1) == record["q"], "Central line image") + need(all(parity(u & v) == (j == k) + for j, u in enumerate(rows) for k, v in enumerate(rows)), "Orthogonal K") + need(all((mv(transpose(rows), x).bit_count() - x.bit_count() - 2 * parity(z & x)) % 4 == 0 + for x in range(SIZE)), "Signed absolute-phase centralizer") + ri, rj = records[:2] + need(A[0][1] == F(-1, 2), "Actual off-diagonal source coefficient") + actual = block(ri, rj, {1: F(1)}, A[0][1]) + formal = {1: A[0][1]} + need(actual == {22: F(1, 2)} and actual != formal, "First physical C != scalar A witness") + need(block(ri, rj, {1: F(1)}, A[0][1], unsigned=True) == {22: F(-1, 2)}, + "Omitted K phase changes exact signed witness") + v = {0: (F(1), F(0))} + cq = sparse_block(ri, rj, sparse_q(v), A[0][1]) + qc = sparse_q(sparse_block(ri, rj, v, A[0][1])) + need(cq != qc, "Commuting C through Q is rejected") + y_only = sparse_q(sparse_block(ri, rj, {1: (F(1), F(0))}, A[0][1]), inverse=True) + need(y_only != qc, "Old Y-only backward Q^2 conjugation is rejected") + + # Independent direct modular address oracle includes actual Q and all eight D axes. + need(IMAG * IMAG % P == P - 1, "Valid exact Gaussian-rational reduction") + modes = [[(i, sign) for i, sign in enumerate(column) if sign] for column in columns] + y = empty() + y[1][1] = 1 + c_y = physical_code(y, records, modes) + x_after_b = add(empty(), gaussian(gaussian(c_y, [0]), range(1, 9)), sign=-1) + y_after_b = gaussian(y, range(1, 9)) + query = gaussian(scalar_code(x_after_b, modes, inverse=True), [0], inverse=True) + y_after_pair = add(y_after_b, query) + residual = gaussian(add(y, scalar_code(c_y, modes, inverse=True), sign=-1), range(1, 9)) + need(y_after_pair == residual and any(any(row) for row in residual), "Actual D(I-A^-1 C) y residual") + # The actual x-only boundary cannot alter the retained y block. + x_after_boundary = scalar_code(x_after_b, modes, inverse=True) + expected_x = add(empty(), gaussian(gaussian(y, [0]), range(1, 9)), sign=-1) + need(x_after_boundary != expected_x, "Actual x-only output boundary also differs") + diagnostic = scalar_code(gaussian(residual, range(1, 9), inverse=True), modes) + expected = add(scalar_code(y, modes), c_y, sign=-1) + need(diagnostic == expected, "Invertible diagnostic A D^-1 yields (A-C)y") + need(diagnostic[0][1] == diagnostic[0][22] == -pow(2, -1, P) % P, + "Literal diagnostic output coefficient") + a_y = scalar_code(y, modes) + formal_query = gaussian(scalar_code(gaussian(gaussian(a_y, [0]), range(1, 9)), modes, inverse=True), [0], inverse=True) + need(formal_query == y_after_b, "Scalar-A predecessor positive control cancels") + helpers = {("helper", k) for k in range(408)} + owned = {("mode", k) for k in range(8)} | {("query", k) for k in range(112)} + cleanup = [("CLEAR", ("mode", k)) for _ in range(6) for k in range(8)] + cleanup += [(op, ("query", k)) for op in ("CLEAR", "ERASE") for k in range(112)] + def check_cleanup(word): + need(all(target in owned and target not in helpers for _, target in word), + "Arbitrary helper owner was changed or erased") + check_cleanup(cleanup) + try: + check_cleanup(cleanup + [("ERASE", ("helper", 17))]) + except ValueError as error: + need("erased" in str(error), "Helper rejection reason") + else: + raise ValueError("Arbitrary helper erasure accepted") + return {"status": "PASS_CODED_REVERSE_PHYSICAL_PAIR_GAP", + "scope": "First literal PR4940 pair under the signed PR4933 physical binding; no general caller obstruction", + "width": 1, "owners": OWNERS, "addresses_per_owner": SIZE, + "chronological_cut": {"p": 19, "backward_stage": 37, "next_thin_stage": 38, + "intervening_bridge_or_idle": False}, + "exact_witness": {"source_port": 1, "destination_port": 0, "input_address": 1, + "A_01": "-1/2", "C_01_output": {"22": "1/2"}, + "A_01_output": {"1": "-1/2"}, + "diagnostic_A_Dinv_y": {"1": "-1/2", "22": "-1/2"}}, + "modular_oracle": {"prime": P, "i": IMAG, "actual_D_axes": list(range(1, 9)), + "nonzero_residual_coordinates": sum(bool(v) for row in residual for v in row)}, + "pair_y_to_y_block": "D*(I-A^-1*C)", + "all_width_argument": "Evaluate each signed K tensor lift inside each owner block; A is applied once. C_f != A tensor I at every f>=1 and D_f is invertible.", + "independent_helper_owners": len(helpers), + "controls": ["scalar-A predecessor cancels", "omitted K sign changes witness", "C-Q commutation fails", "Y-only backward convention fails", "arbitrary helper erasure rejected"], + "local_invoice": {"paid_gaussian_profile": {"1": 2313, "2": 412, "3": 510, "4": 127, "5": 40}, + "native_helper_profile_retained": {"4": 28, "7": 7, "8": 47, "9": 326}, + "native_wrapper_maps_upper": 896, "thin_inverse_query_pauli_maps": 112, + "scalar_A_or_Ainv_evaluations": 3, "recoding_adds": 2688, + "query_destination_adds": 112, "owned_recoding_clears": 48, + "owned_query_initial_clears": 112, "owned_query_copies": 112, + "owned_query_erasures": 112, "peak_added_owned_fields": 120, + "new_recursive_jobs_beyond_native": {"1": 112}, + "denominators": [4, 52], + "unknown_not_zero": ["inherited native ordinary work", "fixed-tape matching/routing and field-map tariff", "odd-denominator precision and rounding", "whole-controller productive endpoint and compiler"]}} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + result = run() + path = HERE / "RESULT.json" + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(json.loads(path.read_text()) == result, "Changed mathematical receipt") + print(result["status"]) + + +if __name__ == "__main__": + main()