From 0ff4a9f9cf763d5fa385d674fea915da53792078 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Fri, 30 Oct 2026 23:15:13 +0800 Subject: [PATCH 1/2] Prove safe nonlinear dual-exchange fusion and exact observer boundaries Prepared for @CubeJerry with coordinated OpenAI Codex assistance. Credit Nick Petalas PR6280 and Ali Romman PR5611/5602 for the retained exchange compiler and tariff, and the P104 lineage. No new kappa. --- .../ORIGIN.json | 9 + .../dual-exchange-independent-audit/PROOF.md | 242 ++++++++++++++ .../dual-exchange-independent-audit/README.md | 106 ++++++ .../SOURCES.json | 24 ++ .../dual-exchange-independent-audit/TASK.json | 110 +++++++ .../VERIFY.json | 61 ++++ .../independent_nonlinear.py | 54 +++ .../noncommutative.py | 128 ++++++++ .../source/compiler.py | 73 +++++ .../dual-exchange-independent-audit/verify.py | 310 ++++++++++++++++++ 10 files changed, 1117 insertions(+) create mode 100644 research/dual-exchange-independent-audit/ORIGIN.json create mode 100644 research/dual-exchange-independent-audit/PROOF.md create mode 100644 research/dual-exchange-independent-audit/README.md create mode 100644 research/dual-exchange-independent-audit/SOURCES.json create mode 100644 research/dual-exchange-independent-audit/TASK.json create mode 100644 research/dual-exchange-independent-audit/VERIFY.json create mode 100644 research/dual-exchange-independent-audit/independent_nonlinear.py create mode 100644 research/dual-exchange-independent-audit/noncommutative.py create mode 100644 research/dual-exchange-independent-audit/source/compiler.py create mode 100644 research/dual-exchange-independent-audit/verify.py diff --git a/research/dual-exchange-independent-audit/ORIGIN.json b/research/dual-exchange-independent-audit/ORIGIN.json new file mode 100644 index 0000000000..43c70e50b8 --- /dev/null +++ b/research/dual-exchange-independent-audit/ORIGIN.json @@ -0,0 +1,9 @@ +{ + "source_pr": 6280, + "source_head": "4d6e4374d6fdda7df72ddeb19dd6756353383346", + "source_path": "research/division-free-dual-exchange/compiler.py", + "git_blob": "9ead98d5735474d1fd35b101a1f4d50426b7e943", + "sha256": "9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf", + "local_path": "source/compiler.py", + "copyright": "Nick Petalas; Apache-2.0. Retained unchanged." +} diff --git a/research/dual-exchange-independent-audit/PROOF.md b/research/dual-exchange-independent-audit/PROOF.md new file mode 100644 index 0000000000..91089f8502 --- /dev/null +++ b/research/dual-exchange-independent-audit/PROOF.md @@ -0,0 +1,242 @@ +# Safe fusion of the PR6280 dual-exchange consumer + +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +The exchange and its compiler are Nick Petalas's PR6280; the source dual-pair +interface and scalar tariff are Ali Romman's PR5611/5602. Conjugation, +retractions and cancellation of inverse basis changes are classical. + +This package independently checks the exact emitted exchange and supplies a +composition contract, including the precise boundary at which fusion is legal. +It does not identify an actual P104 cut satisfying that contract. No new κ. + +## 1. Typed algebra and the source implementation + +Let X and Z be modules, and let A:X→Z and B:Z→X be module homomorphisms with +AB=I_Z. Set Q=I_X−BA. Then Q²=Q, QB=0 and AQ=0. On X⊕Z define + + S(x,z) = (Qx+Bz, Ax), S = [[Q,B],[A,0]]. + +The identities S²=I and the following chronological factorizations use only +AB=I; neither BA=I nor any operator commutation is permitted: + + U_B; L_(-A); U_B; D = S, + D; L_A; U_(-B); L_A = S, + +where U_B(x,z)=(x+Bz,z), L_A(x,z)=(x,z+Ax) and D(x,z)=(x,−z). +For example the first program reaches (x+Bz,−Ax), then (Qx+Bz,−Ax), +then S(x,z). The second reaches (x,Ax−z), then (Qx+Bz,Ax−z), then S(x,z). + +The pinned `compiler.py` is retained unchanged, including its author notice. +For scalar row a and column b in D=Z[1/2], it specializes A=(a_i I_Z)_i, +B=(b_i I_Z)_i. An upper block consists of ADDs to distinct data destinations +with the unchanged spare as source. A lower block consists of ADDs into the +spare from unchanged data sources. Consequently each emitted block has the +displayed action, regardless of zero coefficients. The source branches emit +exactly the two words above; the sole SCALE is the sign on the spare. This +source-reading argument covers every accepted dimension and coefficient, while +the finite emitter checks are regression evidence rather than its proof. + +`noncommutative.py` is an independently written symbolic certificate. Its +letters have the types above; G,H,J are Z→Z. The only reduction is AB→I_Z. +This length-reducing rule has no overlapping redexes, so reduction terminates +with a unique normal form. Every polynomial equality it checks is therefore +valid under substitution of these typed homomorphisms. It checks both source +factorizations, S², the one-use consumer and ordered two/three-use identities. +It does not import the author's dense verifier or infer a theorem from matrix +samples. The separate source-emitter regression does use exact input-basis +execution and is explicitly not claimed to be another universal proof. + +## 2. The consumer needs no linearity of its inner map + +Let G:Z→Z be any function. It need not be additive, invertible, homogeneous, +or commute with scalar multiplication. Apply S, replace the spare by G of +its current value, and apply S again. Direct substitution gives + + (x,z) → (F_G(x),z), + F_G(x) = Qx + B G(Ax) = x + B(G(Ax)−Ax). (1) + +In particular every arbitrary incoming spare is restored and absent from +the resulting data. This is an extension of the source's stated D-linear-G +contract, not a correction of an erroneous source claim. The symbolic +noncommutative certificate concerns linear G; the direct substitution above +supplies the more general set-map statement. Exact nonlinear fixtures +corroborate that distinction without proving it by enumeration. + +Equation (1) implies AF_G=GA. Therefore, for any H:Z→Z, + + F_H(F_G(x)) = x+B(H(G(Ax))−Ax) = F_(H∘G)(x). (2) + +Also F_id=I_X. This is an injective semigroup representation: AF_GB=G. +If G is bijective, F_G has inverse F_(G^-1); conversely bijectivity of F_G +forces bijectivity of G, by the decomposition X=ker(A)⊕im(B). These +properties are algebraic consequences, not admissions of arbitrary functions +as legal recursive children. + +## 3. Exact closed-macro bill and its observation boundary + +Fix the same pair (A,B), same physical fields and spare, and common chart +throughout a sequence. Suppose the only intervening actions are G_1,…,G_k +on that spare, with no observation or modification of a restored full-call +state between them. For k≥1, the chronological programs + + S;G_1;S; S;G_2;S; ... ;S;G_k;S + S;G_1;G_2; ... ;G_k;S (3) + +have the same complete endpoint (F_(G_k∘...∘G_1)(x),z). This follows either +from (2) or exact cancellation of each adjacent S;S. It preserves every G_i +in its original order. No contraction, productive credit or paid recursive +call is removed by this argument. + +For the exact PR5602 ADD tariff let A_a and A_b be the sums of the nonzero +coefficient costs in a and b. The source's chosen exchange has allowance + + B_ex = 2 + min(2 A_a+A_b, A_a+2 A_b). + +Thus the first program in (3) has 2k B_ex scalar allowance, while the second +has 2 B_ex. Both still owe the same k applications of G_i, their native and +delivery costs, and any enclosing allocation, routing, chart and cleanup +costs. For a=(3,5), b=(2,−1), the retained emitter has seven scalar ADD/SCALE instructions and +B_ex=64. The closed three-call macro changes 42 such instructions/384 allowance +to 14 instructions/128 allowance, retaining all three uses. This is an exact local +invoice comparison, not a wall-time measurement or a supplier improvement. + +The missing intermediate boundary is substantive. After the j-th use in the +fused program the actual representation is + + (Qx+Bz, (G_j∘...∘G_1)(Ax)), + +whereas a separately returned consumer presents + + (Qx+B(G_j∘...∘G_1)(Ax), z). + +A caller expecting the latter may distinguish them. In the named pair, start +at (x_0,x_1,z)=(1,0,7) and use G(t)=t+1. The fused internal state is +(9,−4,4), while the returned consumer state is (3,−1,7). Even reading the +spare separates them. A caller may instead implement a correctly transformed +observer, but that observer and its cost are outside this theorem. The theorem +does not promise equal outputs under interruption, exceptions, rounding, +interleaved access, or a change of chart/pair between the retained uses. + +Every source exchange's elementary scalar-prefix bound remains valid relative +to its own entrance. No magnitude or error bound for arbitrary G_i, or for +the complete nonlinear macro, is inferred from those exchange bounds. + +## 3a. Exact class of safe read-only intermediate observers + +The no-observer condition above has a precise relaxation. Fix a deterministic +read-only observer O:X⊕Z→Y, with no mutation, control-flow change or alteration +of any subsequent G_i. Require the same observation at each internal fused +state and its corresponding returned consumer state, for **every** incoming +state and **every** sequence of inner functions. This universal observation +contract holds exactly when + + O∘S = O. (5) + +Indeed the returned state is S applied to the fused state, so (5) suffices. +For necessity choose all inner functions to be identity. Then the internal +state is S(x,z), which ranges over all X⊕Z because S is an involution. +Thus equality of observations forces (5) on every state. Equivalently, in the +split coordinates x=k+Bw with k∈ker(A), S swaps w and z; an allowed observer +must be symmetric in those two coordinates with k fixed. + +If Y is a module and O is module-linear, write O(x,z)=Cx+Dz, where C:X→Y and +D:Z→Y are homomorphisms. Equation (5) is equivalent to + + D=CB, and therefore O(x,z)=C(x+Bz). (6) + +To see necessity, set x=0 in O(S(x,z))=O(x,z). To see sufficiency, the +x-coefficient after exchange is CQ+DA=C−CBA+CBA=C, and the z-coefficient is +CB=D. No division by two, commutation or faithful scalar representation is +needed. The exact linear observation defect is +`O(S(x,z))−O(x,z)=(D−CB)(Ax−z)`. +In particular observers factoring through Qx are allowed because +QB=0. Nonlinear observers are governed by (5), not merely the linear form +(6); for example, when Z=Q the product (Ax)z is invariant under the swap. + +Universality matters. For a fixed nonsurjective inner map, it is necessary +only to agree on states actually reached and their exchanged partners. For +X=Z=Q and A=B=identity, choose G=0 and O(x,z)=xz². The relevant states are +(z,0) and (0,z), where both observations vanish, although O(1,2)=4 differs +from O(2,1)=2. This is a counterexample to asserting global swap-invariance +as a necessary condition for one fixed non-surjective call, not a failure of +the universal contract above. + +These observations retain their original cost in the fused macro. An actual +caller must establish that the observer can legally read those physical +fields in the common chart; algebraic invariance supplies no free delivery, +extra ownership, implementation or observer transformation. The existing +exception, rounding and interruption limitations remain. Arbitrary observers, +mutating actions and observer-dependent control flow are outside this extension. + +## 4. Matching boundary pairs is necessary, not just convenient + +Let the entering exchange use (A,B) with AB=I_Z, and the exiting exchange use +(C,D) with CD=I_Z on the same typed modules. Direct expansion yields + + z_out = C(I−BA)x + CBz, + x_out = (I−DC)(I−BA)x + (I−DC)Bz + D G(Ax). (4) + +These formulas hold for every function G. Restoring z for every x,z forces +CB=I_Z and C(I−BA)=0. Hence C=CBA=A. Conversely C=A restores the spare. +Once C=A, the dirty-spare coefficient in the data is B−D. Independence of +the data output from every z is therefore equivalent to D=B. Thus the full +arbitrary-spare return/no-leakage contract holds exactly when the two pairs +match. This is equality of module maps: the scalar coefficient conclusion +uses the faithful scalar field-value modules of the source interface. + +Both duality constraints alone are insufficient. Over Q, take A=(1,0), +B=(1,0)^T and G=identity. Choosing C=A,D=(1,1)^T preserves z but sends +(0,0,1) to (0,−1,1), leaking spare data. Choosing C=(1,1),D=B instead +sends (0,1,0) to (−1,1,1), failing spare restoration. The verifier executes +these counterexamples with the actual emitted programs. They are failures +of the mismatched extension, not counterexamples to PR6280's matching-pair +claim. More general basis maps satisfying the same row/column equations may +differ on ker(A); this package does not license substituting only one half +of such a different completion. + +## Scope, evidence and credit + +The scientific base is `2485805a6d47f36ea83ddde6327d453ac82d44dc`; the exact +pending source is PR6280 `4d6e4374d6fdda7df72ddeb19dd6756353383346`. +`ORIGIN.json` records the original compiler path, Git blob and SHA256. It +was read from that Git object and copied byte for byte. The source commit is +not made an ancestor of this contribution, so the base source-history check +does not assert pending-PR ancestry. The standalone checker authenticates +both the SHA256 and the Git-blob encoding before source execution. + +The source compiler's bounded algebraic input contract is broader than the +actual caller's coefficient-magnitude admission. The accepted pair +a=(2^63,1),b=(0,1) emits a coefficient violating |q|+1<2^16. This documented +positive discriminator prevents treating compiler acceptance as caller +admission; it is already a limitation of the predecessor, not a newly found bug. + +No actual P104 interval with the closed-macro contract is supplied. Physical +availability of the spare, native charts and phases, arbitrary-input caller +bindings, complete signed moments, precision, tape/stock, completion/compiler +and analytic recovery remain separate obligations. The selected κ=.003125804 +and all five framework assumptions are unchanged. There is no Lean proof, +independent human theorem review, or complete multiplication theorem here. + +Credit Nick Petalas for PR6280's exchange/compiler and its 134→64 comparison; +Ali Romman for PR5611/5602 and the retained P104 helper/compiler lineage; +Chris R/Clear1nsight's `p104-joint-compensation` for an earlier distinct +free-operator compensator certificate. None of those results is claimed as +new. The new work is the source-bound safe-fusion contract, boundary matching +theorem, independent block certificate and controls, developed by the +exchange-audit research subagent and reviewed within the coordinated run. +The exact read-only observer refinement was independently derived and checked +by research worker A, using the split-coordinate swap and explicit reachability +quantifiers; it is part of the same closed-macro contribution. + +## Independent exhaustive nonlinear corroboration + +A separate lead-review implementation authenticates the original source +emitter, reduces its named (3,5)/(2,-1) pair to F3, and interprets the emitted +gates without importing the primary verifier or polynomial engine. It covers +every pair of the 27 functions F3→F3, every 27 three-role input, and all three +emitter choices: 59,049 cases. Literal separate consumers, the fused consumer +and the direct nonlinear endpoint formula agree. Both ordinary and optimized +runs are registered. A different valid dual column produces explicit dirty-spare +leakage and is rejected as a matching-boundary substitution. This finite +corroboration does not replace the module/set-map proof or supply a native +implementation. The independent program is `independent_nonlinear.py`. diff --git a/research/dual-exchange-independent-audit/README.md b/research/dual-exchange-independent-audit/README.md new file mode 100644 index 0000000000..19bd5545e9 --- /dev/null +++ b/research/dual-exchange-independent-audit/README.md @@ -0,0 +1,106 @@ +# Safe fusion of division-free dual-exchange consumers + +For the exact PR6280 exchange compiler, a closed sequence of k same-pair +consumers needs only two exchanges, with scalar allowance **2B rather than +2kB**, while retaining every inner call. For its a=(3,5), b=(2,−1) example, +a closed three-call sequence has **128 rather than 384 scalar allowance** +(14 rather than 42 scalar gates), plus the same three inner calls and all +other delivery costs. **No new κ.** + +This is a scoped algebraic composition result and independent source audit. +It supplies no actual P104 interval where fusion is legal. Cancellation of +inverse basis changes is classical; the contribution is the exact +source-bound contract, complete local bill and failure boundaries. + +## Result and limits + +[PROOF.md](PROOF.md) proves the arbitrary-spare identity for any inner +function G, including nonlinear functions, and the ordered semigroup law +F_H∘F_G=F_(H∘G). It also proves that matching dual pairs are necessary and +sufficient for the entering/exiting exchanges to restore the arbitrary +spare and prevent its leakage into the data. These extend the predecessor's +one-use linear-operator statement; no error in that statement is asserted. + +The fused internal representation differs from a returned consumer state. +An explicit observer distinguishes them. Fusion therefore requires a fixed +pair/chart/spare and no intermediate modification of the restored full-call +state. Read-only observations are permitted exactly when **O∘S=O** for the +universal all-inner-maps contract; a linear observer O(x,z)=Cx+Dz qualifies +exactly when D=CB. The proof distinguishes this universal condition from the +weaker condition on states reachable under one fixed nonsurjective call, and +retains every observation cost and physical access obligation. It does not supply exception-safe intermediate +return, rounded-error bounds, native scheduling, or new productive credit. + +The independent symbolic certificate reduces only AB=I in a typed free +operator algebra. It permits no commutations. The actual source emitter is +then checked separately on exact coefficients; the author's dense verifier +and scientific suite are never imported. The nonlinear theorem rests on +direct substitution, while nonlinear executions are corroborating evidence. + +## Evidence and source pins + +Canonical base: `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. +Selected κ remains `781451/250000000` with all five framework assumptions. +Pending PR6280 source: `4d6e4374d6fdda7df72ddeb19dd6756353383346`. +[ORIGIN.json](ORIGIN.json) records its exact compiler path, Git blob and +SHA256; only that compiler is retained, unchanged. [SOURCES.json](SOURCES.json) +pins the originating task/selected record and actual PR5602 caller tariff. + +The pending source commit is not merged or made ancestral here. Its compiler +is authenticated by byte equality/SHA256/Git-blob encoding; any base-history +check covers the base-origin pins, not pending-PR ancestry or admission. + +The registered verifier covers: + +- Seven universal free-block equalities and four nonzero symbolic defects. +- 131 deterministic emitter requests through every dimension 1–16 and boundary + coefficients, all three factorization modes: 393 checks, including exact + scalar tariff and every scalar-prefix envelope. +- 225 nonlinear arbitrary-spare cases at one, two and three uses. +- Nine exact-reason rejecting controls, including three actual source mutations. +- 1,500 linear and 375 nonlinear invariant-observer comparisons, plus controls + distinguishing forbidden observers and fixed-map reachability from universal + invariance. These corroborate the separate quantified proof. +- Concrete observer and two mismatched-dual-pair counterexamples, plus a + compiler-accepted coefficient that the actual caller's magnitude cap excludes. + +Normal and optimized warning-strict CPython 3.12 commands are registered. +The source compiler accepts a broader bounded algebraic domain than the +actual caller; that inherited distinction remains explicit. No full selected +cold replay, physical caller, all-size compiler/precision/tape proof, Lean +build, hosted-CI pass or independent human theorem review is claimed. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/dual-exchange-independent-audit +``` + +Expected scientific status: `PASS_DUAL_EXCHANGE_FUSION_AUDIT`; launcher: +`PASS_REGISTERED_RESEARCH_PACKAGE`. Direct `python3 -I -W error -B +research/dual-exchange-independent-audit/verify.py` also works in a source +export containing its one declared external input. Add `-O` for the second +registered mode. It prints a generated receipt without writing evidence files. + +## Open next questions + +Find one literal current P104 interval with two same-pair uses, unchanged +charts/ownership and only compatible read-only intermediate observations. Trace every field +read/write and retain every native/recursive call before claiming the local +allowance saving applies there. No such source interval is established in +this package, and its absence blocks any supplier-level consequence. + +## Credit + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance by the +exchange-audit research subagent, with separate adversarial proof review and +lead-orchestrator verification. Nick Petalas retains PR6280's exchange, +emitter and prior 134→64 comparison. Ali Romman retains PR5611/5602 and the +P104 helper/caller lineage. Chris R/Clear1nsight's earlier distinct +`p104-joint-compensation` package is credited for its free-operator method. +The source notice is preserved. New work is Apache-2.0; no literature-wide +priority claim is made for retractions, conjugation or cancellation. + +The registered replay also includes an independent lead-review field interpreter covering all 59,049 F3 function-pair/input/emitter cases for the named nonunit pair, plus a mismatched-pair leakage control. diff --git a/research/dual-exchange-independent-audit/SOURCES.json b/research/dual-exchange-independent-audit/SOURCES.json new file mode 100644 index 0000000000..a516f47163 --- /dev/null +++ b/research/dual-exchange-independent-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-coupled-helper-bases/local.py", + "usage": "input", + "git_blob": "9556e86744e18efdd76263a36664830c695f1c0f", + "sha256": "5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925" + } + ] +} diff --git a/research/dual-exchange-independent-audit/TASK.json b/research/dual-exchange-independent-audit/TASK.json new file mode 100644 index 0000000000..3b4965ff9c --- /dev/null +++ b/research/dual-exchange-independent-audit/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Source-bound independent algebraic audit and safe-fusion theorem for PR6280 dual-exchange consumers, including arbitrary inner functions and exact observer/pair-matching boundaries.", + "scope_change_reason": "The assigned formal-interface card is narrowed to a written quantified interface proof and independent free-operator certificate for the newly published PR6280 emitter; no proof-assistant or selected-assumption discharge is claimed.", + "bottleneck_link": "Repeated scalar basis preparation may be removed only within a closed consumer macro. This proves the exact local tariff and ABI boundary, while leaving actual P104 applicability and all paid native calls open.", + "budget_minutes": 90, + "stop_rule": "Stop after the same-pair composition theorem, arbitrary-spare boundary characterization, and source-bound controls; do not launch a physical cut search or claim supplier admission.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py and noncommutative.py; normal/optimized registered checks. Exact predecessor in ORIGIN.json.", + "author": "@CubeJerry with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance, including exchange-audit subagent construction and separate adversarial proof review; no independent human or formal-kernel acceptance. Research worker A independently derived and checked the exact invariant-observer class and its reachability limitation.", + "open_questions": [ + { + "question": "Does an actual current P104 caller contain at least two same-pair uses with only compatible read-only intermediate observations and unchanged chart/ownership?", + "why_it_matters": "Only such a source-bound interval can realize the proven scalar saving without adding a new boundary cost.", + "first_step": "Identify one literal interval and its frames, field ownership, source accesses and native uses; compare its full event sequence against the closed-macro contract.", + "blocked_by": "No such actual caller interval or compatible chart/ownership proof is supplied." + } + ], + "track_seed": 79, + "selected_context": { + "kappa": "781451/250000000", + "priority_revision": 8, + "source_pr": 6030, + "five_framework_assumptions_unchanged": true + }, + "scope_allocation": { + "chosen": "independent free-operator consumer and exact safe fusion", + "alternatives": [ + "actual selected-cut installation, deferred", + "rounded prefix amplification, deferred" + ] + }, + "overlap_coverage": "Root checked live PR bodies and bounded all-state exchange/nonlinear searches; narrow main README search found the distinct p104-joint-compensation precedent. Discussion posting unavailable; no exhaustive novelty claim." +} diff --git a/research/dual-exchange-independent-audit/VERIFY.json b/research/dual-exchange-independent-audit/VERIFY.json new file mode 100644 index 0000000000..33b7340929 --- /dev/null +++ b/research/dual-exchange-independent-audit/VERIFY.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-coupled-helper-bases/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Seven typed free-block identities, actual source-emitter tariff/prefix regression, nonlinear dirty-input fusion, exact-reason source/semantic controls and observer/pair-mismatch boundaries." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Seven typed free-block identities, actual source-emitter tariff/prefix regression, nonlinear dirty-input fusion, exact-reason source/semantic controls and observer/pair-mismatch boundaries." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_nonlinear.py" + ], + "timeout_seconds": 60, + "checks": "Independent exhaustive F3 function-pair composition:59049 cases across all source emitter modes and mismatched-pair leakage control." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/independent_nonlinear.py" + ], + "timeout_seconds": 60, + "checks": "Independent exhaustive F3 function-pair composition:59049 cases across all source emitter modes and mismatched-pair leakage control." + } + ] +} diff --git a/research/dual-exchange-independent-audit/independent_nonlinear.py b/research/dual-exchange-independent-audit/independent_nonlinear.py new file mode 100644 index 0000000000..2d96b84672 --- /dev/null +++ b/research/dual-exchange-independent-audit/independent_nonlinear.py @@ -0,0 +1,54 @@ +"""Independent exhaustive nonlinear composition check over F3. + +Jerry Chen (@CubeJerry), OpenAI Codex lead-agent assistance. Apache-2.0. +This uses the authenticated source emitter, with a separate field interpreter +and direct endpoint formula; it imports no primary verifier or polynomial engine. +""" +from pathlib import Path +import itertools, runpy, hashlib, json +from fractions import Fraction +source=Path(__file__).resolve().parent/'source/compiler.py' +raw=source.read_bytes() +if hashlib.sha256(raw).hexdigest()!='9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf': + raise ValueError('source compiler hash mismatch') +mod=runpy.run_path(str(source)) +a,b=(3,5),(2,-1) +def f3(q): + q=Fraction(q) + return q.numerator*pow(q.denominator,-1,3)%3 +def execute(word,state): + state=list(state) + for op,d,s,q in word: + if op=='ADD': state[d]=(state[d]+q*state[s])%3 + elif op=='SCALE': state[d]=q*state[d]%3 + else: raise ValueError(op) + return tuple(state) +def consumer(word,f,state): + t=execute(word,state) + t=(*t[:2],f[t[2]]) + return execute(word,t) +cases=0 +functions=list(itertools.product(range(3),repeat=3)) +states=list(itertools.product(range(3),repeat=3)) +for repeat in ['a','b','cheapest']: + word=[(op,d,s,f3(q)) for op,d,s,q in mod['compile_exchange'](a,b,repeat)] + for f,g in itertools.product(functions,repeat=2): + composed=tuple(g[f[t]] for t in range(3)) + for x in states: + separate=consumer(word,g,consumer(word,f,x)) + fused=consumer(word,composed,x) + t=(a[0]*x[0]+a[1]*x[1])%3 + oracle=((x[0]+b[0]*(composed[t]-t))%3,(x[1]+b[1]*(composed[t]-t))%3,x[2]) + if separate!=fused or fused!=oracle: + raise ValueError((repeat,f,g,x,separate,fused,oracle)) + cases+=1 +# Distinct pairs may each satisfy duality yet leak arbitrary spare values. +incoming=[(op,d,s,f3(q)) for op,d,s,q in mod['compile_exchange']((1,1),(1,0))] +outgoing=[(op,d,s,f3(q)) for op,d,s,q in mod['compile_exchange']((1,1),(0,1))] +leak=[] +for z in range(3): + after=execute(incoming,(0,0,z)) + result=execute(outgoing,after) + leak.append(result) +if leak!=[(0,0,0),(1,2,1),(2,1,2)]: raise ValueError(leak) +print(json.dumps({'status':'PASS_INDEPENDENT_NONLINEAR_EXCHANGE_COMPOSITION','cases':cases,'pair':{'a':a,'b':b},'domain':'every F3 scalar map pair, every three-role F3 input, all three emitter modes','source_sha256':hashlib.sha256(raw).hexdigest(),'mismatched_column_leak':leak},indent=2)) diff --git a/research/dual-exchange-independent-audit/noncommutative.py b/research/dual-exchange-independent-audit/noncommutative.py new file mode 100644 index 0000000000..ccf5804214 --- /dev/null +++ b/research/dual-exchange-independent-audit/noncommutative.py @@ -0,0 +1,128 @@ +"""Independent free-block certificate for the PR6280 consumer. + +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +Only AB=1 is reduced. In particular BA, GA and BG are not commuted. +""" +from fractions import Fraction + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def normal(word): + """Unique normal form: the length-reducing rule AB -> empty has no overlaps.""" + stack = [] + for letter in word: + if stack and stack[-1] == "A" and letter == "B": + stack.pop() + else: + stack.append(letter) + return tuple(stack) + + +def atom(name): + return {(name,): Fraction(1)} + + +ZERO = {} +ONE = {(): Fraction(1)} + + +def add(*terms): + answer = {} + for term in terms: + for word, coefficient in term.items(): + answer[word] = answer.get(word, 0) + coefficient + return {w: c for w, c in answer.items() if c} + + +def scale(term, coefficient): + return {w: c * coefficient for w, c in term.items() if c * coefficient} + + +def mul(*terms): + answer = ONE + for term in terms: + products = {} + for left, lc in answer.items(): + for right, rc in term.items(): + key = normal(left + right) + products[key] = products.get(key, 0) + lc * rc + answer = {w: c for w, c in products.items() if c} + return answer + + +def mm(left, right): + return [[add(*(mul(left[i][k], right[k][j]) for k in range(2))) + for j in range(2)] for i in range(2)] + + +def chain(*chronological): + value = [[ONE, ZERO], [ZERO, ONE]] + for step in chronological: + value = mm(step, value) + return value + + +def typed(matrix): + """A:X->Z, B:Z->X, and G/H/J:Z->Z; each block has its actual type.""" + types = {"A": ("X", "Z"), "B": ("Z", "X"), + "G": ("Z", "Z"), "H": ("Z", "Z"), "J": ("Z", "Z")} + objects = ("X", "Z") + for i in range(2): + for j in range(2): + for word in matrix[i][j]: + current = objects[j] + for letter in reversed(word): + domain, codomain = types[letter] + require(current == domain, "ILL_TYPED_WORD") + current = codomain + require(current == objects[i], "ILL_TYPED_BLOCK") + + +def check(): + a, b, g, h, j = (atom(s) for s in "ABGHJ") + q = add(ONE, scale(mul(b, a), -1)) + s = [[q, b], [a, ZERO]] + upper = [[ONE, b], [ZERO, ONE]] + lower = [[ONE, ZERO], [a, ONE]] + upper_negative = [[ONE, scale(b, -1)], [ZERO, ONE]] + lower_negative = [[ONE, ZERO], [scale(a, -1), ONE]] + sign = [[ONE, ZERO], [ZERO, scale(ONE, -1)]] + ident = [[ONE, ZERO], [ZERO, ONE]] + + def use(f): + return [[ONE, ZERO], [ZERO, f]] + + def induced(f): + return [[add(q, mul(b, f, a)), ZERO], [ZERO, ONE]] + + equations = { + "repeat_b": (chain(upper, lower_negative, upper, sign), s), + "repeat_a": (chain(sign, lower, upper_negative, lower), s), + "involution": (chain(s, s), ident), + "one_consumer": (chain(s, use(g), s), induced(g)), + "ordered_composition": (chain(induced(g), induced(h)), induced(mul(h, g))), + "three_consumer_fusion": ( + chain(s, use(g), s, s, use(h), s, s, use(j), s), + chain(s, use(g), use(h), use(j), s)), + "three_consumer_target": ( + chain(s, use(g), use(h), use(j), s), induced(mul(j, h, g))), + } + for name, (actual, expected) in equations.items(): + typed(actual) + typed(expected) + require(actual == expected, "NC_IDENTITY_" + name) + # These are nonzero symbolic defects, not failures of a sampled matrix. + defects = { + "native_order": chain(s, use(h), use(g), s) != induced(mul(h, g)), + "missing_final_exchange": chain(s, use(g)) != induced(g), + "omitted_sign": chain(upper, lower_negative, upper) != s, + "BA_not_identity": mul(b, a) != ONE, + } + require(all(defects.values()), "NC_CONTROL_DID_NOT_DISTINGUISH") + return {"universal_block_identities": len(equations), + "nonzero_free_defects": len(defects), + "rewrite_relation": "AB=I_Z only; no commutations"} diff --git a/research/dual-exchange-independent-audit/source/compiler.py b/research/dual-exchange-independent-audit/source/compiler.py new file mode 100644 index 0000000000..9ead98d573 --- /dev/null +++ b/research/dual-exchange-independent-audit/source/compiler.py @@ -0,0 +1,73 @@ +"""Division-free dual-pair exchange, produced by Nick Petalas; Apache-2.0.""" + +from fractions import Fraction + +MAX_DIMENSION = 16 +MAX_NUMERATOR_BITS = 64 +MAX_DENOMINATOR_BITS = 33 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def pair(a, b): + """Validate a bounded dyadic dual pair at the public compiler boundary.""" + need(type(a) in (list, tuple) and type(b) in (list, tuple), "Vector containers") + need(1 <= len(a) == len(b) <= MAX_DIMENSION, "Matching bounded dimensions") + need(all(type(q) in (int, Fraction) for q in (*a, *b)), "Exact coefficients") + a, b = tuple(map(Fraction, a)), tuple(map(Fraction, b)) + for q in (*a, *b): + need(abs(q.numerator).bit_length() <= MAX_NUMERATOR_BITS, "Numerator bound") + d = q.denominator + need(d.bit_length() <= MAX_DENOMINATOR_BITS and d & (d - 1) == 0, + "Bounded dyadic denominator") + need(sum(x * y for x, y in zip(a, b)) == 1, "Dual pairing equals one") + return a, b + + +def addition_cost(q): + """PR5602's real scalar ADD allowance for a nonzero dyadic coefficient.""" + q = Fraction(q) + n, d = abs(q.numerator), q.denominator + need(n > 0 and d & (d - 1) == 0, "Nonzero dyadic ADD") + return 2 * (3 + n.bit_length() - 1 + n.bit_count() + d.bit_length() - 1) + + +def allowance(operations): + """Price this compiler's ADDs and its one sign SCALE.""" + need(len(operations) <= 3 * MAX_DIMENSION + 1, "Exchange operation bound") + total = 0 + for op, destination, source, q in operations: + if op == "ADD": + need(destination != source, "Distinct ADD roles") + total += addition_cost(q) + else: + need(op == "SCALE" and destination == source and q == -1, + "Only sign SCALE") + total += 2 + return total + + +def compile_exchange(a, b, repeat="cheapest"): + """Emit S=[[I-ba,b],[a,0]] on n data roles and arbitrary spare role n. + + 'cheapest' minimizes the declared tariff among these two factorizations. + It does not solve unrestricted circuit optimization. + """ + a, b = pair(a, b) + need(repeat in ("a", "b", "cheapest"), "Known factorization") + if repeat == "cheapest": + a_cost = sum(addition_cost(q) for q in a if q) + b_cost = sum(addition_cost(q) for q in b if q) + repeat = "a" if a_cost < b_cost else "b" + spare = len(a) + upper = [("ADD", i, spare, q) for i, q in enumerate(b) if q] + lower = [("ADD", spare, i, q) for i, q in enumerate(a) if q] + sign = [("SCALE", spare, spare, Fraction(-1))] + if repeat == "b": + negative = [(op, r, s, -q) for op, r, s, q in lower] + return upper + negative + upper + sign + negative = [(op, r, s, -q) for op, r, s, q in upper] + return sign + lower + negative + lower diff --git a/research/dual-exchange-independent-audit/verify.py b/research/dual-exchange-independent-audit/verify.py new file mode 100644 index 0000000000..6c2ca4ae70 --- /dev/null +++ b/research/dual-exchange-independent-audit/verify.py @@ -0,0 +1,310 @@ +"""Independent PR6280 consumer-fusion certificate and source-emitter checks. + +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +Only the authenticated emitter, never the predecessor verifier, is executed. +""" +import ast +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from itertools import product +import json +from pathlib import Path +import runpy + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +COMPILER_SHA = "9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf" +COMPILER_BLOB = "9ead98d5735474d1fd35b101a1f4d50426b7e943" +SOURCE_HEAD = "4d6e4374d6fdda7df72ddeb19dd6756353383346" +TARIFF_PATH = "research/p104-coupled-helper-bases/local.py" +TARIFF_SHA = "5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def no_duplicates(pairs): + result = {} + for key, value in pairs: + need(key not in result, "DUPLICATE_JSON_KEY") + result[key] = value + return result + + +def checked_source(raw): + need(sha256(raw).hexdigest() == COMPILER_SHA, "COMPILER_SOURCE_BYTES") + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + need(sha1(blob).hexdigest() == COMPILER_BLOB, "COMPILER_GIT_BLOB") + return raw + + +def load_compiler(raw): + namespace = {"__name__": "audited_compiler"} + exec(compile(raw, "authenticated-PR6280-compiler.py", "exec"), namespace) + return namespace + + +def bindings(): + origin = json.loads((HERE / "ORIGIN.json").read_bytes(), object_pairs_hook=no_duplicates) + need(origin["source_head"] == SOURCE_HEAD and origin["source_pr"] == 6280 + and origin["source_path"] == "research/division-free-dual-exchange/compiler.py" + and origin["local_path"] == "source/compiler.py" + and origin["sha256"] == COMPILER_SHA and origin["git_blob"] == COMPILER_BLOB, + "COMPILER_ORIGIN") + compiler = checked_source((HERE / "source/compiler.py").read_bytes()) + tariff = (ROOT / TARIFF_PATH).read_bytes() + need(sha256(tariff).hexdigest() == TARIFF_SHA, "TARIFF_SOURCE_BYTES") + return compiler, tariff + + +def price_coefficient(value): + """Count the actual tariff by repeated division, with no bit methods.""" + q = Q(value) + numerator, denominator = abs(q.numerator), q.denominator + need(numerator > 0, "NONZERO_ADD_PRICE") + digits = ones = exponent = 0 + while numerator: + numerator, remainder = divmod(numerator, 2) + digits += 1 + ones += remainder + while denominator > 1: + denominator, remainder = divmod(denominator, 2) + need(remainder == 0, "DYADIC_ADD_PRICE") + exponent += 1 + return 2 * (2 + digits + ones + exponent) + + +def price(operations): + total = 0 + for op, target, source, q in operations: + if op == "ADD": + need(target != source, "DISTINCT_ADD_ROLES") + total += price_coefficient(q) + else: + need((op, target == source, q) == ("SCALE", True, -1), "SIGN_SCALE_ONLY") + total += 2 + return total + + +def source_tariff_expression(raw): + matches = [] + for node in ast.walk(ast.parse(raw)): + if isinstance(node, ast.AugAssign) and isinstance(node.target, ast.Name): + if node.target.id == "scalar" and "bit_count" in ast.dump(node.value): + matches.append(node.value) + need(len(matches) == 1, "UNIQUE_SOURCE_ADD_TARIFF") + return compile(ast.Expression(matches[0]), "source-ADD-tariff", "eval") + + +def literal(operations, inputs): + values = list(map(Q, inputs)) + for op, target, source, q in operations: + need(0 <= target < len(values) and 0 <= source < len(values), "ROLE_RANGE") + if op == "ADD": + need(target != source, "DISTINCT_ADD_ROLES") + values[target] += q * values[source] + else: + need(op == "SCALE" and target == source and q == -1, "SIGN_SCALE_ONLY") + values[target] = -values[target] + return values + + +def check_emitter(module, a, b, tariff): + """Secondary code regression; the universal free-block proof is separate.""" + a, b = list(map(Q, a)), list(map(Q, b)) + n = len(a) + need(sum(x * y for x, y in zip(a, b)) == 1, "FIXTURE_DUALITY") + costs = {} + for repeat in ("a", "b", "cheapest"): + ops = module["compile_exchange"](a, b, repeat) + ca = sum(price_coefficient(q) for q in a if q) + cb = sum(price_coefficient(q) for q in b if q) + expected_cost = {"a": 2 + 2 * ca + cb, "b": 2 + ca + 2 * cb, + "cheapest": 2 + min(2 * ca + cb, ca + 2 * cb)}[repeat] + need(price(ops) == expected_cost, "EMITTER_TARIFF") + need(module["allowance"](ops) == expected_cost, "SOURCE_ALLOWANCE") + for op, _, _, q in ops: + if op == "ADD": + source_cost = eval(tariff, {"__builtins__": {}}, + {"n": abs(q.numerator), "d": q.denominator}) + need(source_cost == price_coefficient(q), "ACTUAL_CALLER_TARIFF") + permitted = set(a + b + [-q for q in a + b] + [Q(-1)]) + need(all(q in permitted for _, _, _, q in ops), "NO_NEW_COEFFICIENTS") + alpha, beta = 1 + sum(map(abs, a)), 1 + sum(map(abs, b)) + actual_repeat = repeat if repeat != "cheapest" else ("a" if ca < cb else "b") + envelope = alpha * alpha * beta if actual_repeat == "a" else alpha * beta * beta + columns = [[Q(i == j) for i in range(n + 1)] for j in range(n + 1)] + for step in ops: + columns = [literal([step], c) for c in columns] + need(max(sum(abs(c[i]) for c in columns) for i in range(n + 1)) <= envelope, + "PREFIX_ENVELOPE") + expected = [[Q(i == j) - b[i] * a[j] for i in range(n)] + [a[j]] + for j in range(n)] + [b + [Q(0)]] + need(columns == expected, "EMITTER_BOUNDARY") + repeated, single = (a, b) if actual_repeat == "a" else (b, a) + count = 2 * sum(q != 0 for q in repeated) + sum(q != 0 for q in single) + 1 + need(len(ops) == count, "EMITTER_GATE_COUNT") + costs[repeat] = expected_cost + return costs["cheapest"] + + +def sequence(ops, inputs, functions, fused): + values = list(map(Q, inputs)) + if fused: + values = literal(ops, values) + for fn in functions: + if not fused: + values = literal(ops, values) + values[-1] = fn(values[-1]) + if not fused: + values = literal(ops, values) + if fused: + values = literal(ops, values) + return values + + +def functional_evidence(module): + a, b = list(map(Q, [3, 5])), list(map(Q, [2, -1])) + ops = module["compile_exchange"](a, b) + functions = (lambda t: t * t + 1, lambda t: abs(t) - 2, lambda t: t * t - t) + cases = 0 + for x0, x1, z in product(range(-2, 3), range(-2, 3), (-3, 0, 2)): + original = [Q(x0), Q(x1), Q(z)] + for count in (1, 2, 3): + naive = sequence(ops, original, functions[:count], False) + fused = sequence(ops, original, functions[:count], True) + ax = 3 * original[0] + 5 * original[1] + used = ax + for fn in functions[:count]: + used = fn(used) + target = [original[i] + b[i] * (used - ax) for i in range(2)] + [original[-1]] + need(naive == fused == target, "NONLINEAR_FUSION") + cases += 1 + need((len(ops), price(ops)) == (7, 64), "NAMED_SOURCE_TARIFF") + return {"nonlinear_dirty_input_cases": cases, + "three_call_scalar_gates": {"separate": 42, "fused": 14}, + "three_call_scalar_allowance": {"separate": 384, "fused": 128}, + "native_or_other_function_calls_retained": 3} + + +def observer_evidence(module): + """Finite corroboration of the separately proved universal observer class.""" + ops = module["compile_exchange"]([3, 5], [2, -1]) + functions = (lambda t: t, lambda t: t * t + 1, lambda t: Q(0)) + linear_count = nonlinear_count = 0 + for x0, x1, z in product(range(-2, 3), repeat=3): + for fn in functions: + internal = literal(ops, [x0, x1, z]) + internal[-1] = fn(internal[-1]) + returned = literal(ops, internal) + for c0, c1 in ((1, 0), (0, 1), (3, 5), (-2, 7)): + d = 2 * c0 - c1 + left = c0 * internal[0] + c1 * internal[1] + d * internal[2] + right = c0 * returned[0] + c1 * returned[1] + d * returned[2] + need(left == right, "INVARIANT_LINEAR_OBSERVER") + linear_count += 1 + left = (3 * internal[0] + 5 * internal[1]) * internal[2] + right = (3 * returned[0] + 5 * returned[1]) * returned[2] + need(left == right, "INVARIANT_NONLINEAR_OBSERVER") + nonlinear_count += 1 + internal = literal(ops, [1, 0, 7]) + internal[-1] += 1 + returned = literal(ops, internal) + # C=(1,0), D=3 differs from CB=2 and distinguishes these actual states. + need(internal[0] + 3 * internal[2] != returned[0] + 3 * returned[2], + "NONINVARIANT_OBSERVER_NOT_DISTINGUISHED") + swap = module["compile_exchange"]([1], [1]) + for z in range(-2, 3): + internal = literal(swap, [1, z]) + internal[-1] = Q(0) + returned = literal(swap, internal) + need(internal[0] * internal[1] ** 2 == returned[0] * returned[1] ** 2 == 0, + "FIXED_MAP_REACHABLE_OBSERVER") + need(1 * 2 ** 2 != 2 * 1 ** 2, "FIXED_MAP_NOT_GLOBAL_INVARIANCE") + return {"linear_observation_comparisons": linear_count, + "nonlinear_observation_comparisons": nonlinear_count, + "observer_scope_discriminators": 2, + "contract": "O composed with S equals O universally; linear D=CB", + "all_observation_costs_retained": True} + + +def expect_reject(action, expected): + try: + action() + except ValueError as exc: + need(str(exc) == expected, "WRONG_CONTROL_REASON:" + str(exc)) + return 1 + raise ValueError("CONTROL_ACCEPTED:" + expected) + + +def controls(module, raw, tariff): + rejected = expect_reject(lambda: checked_source(raw + b"\n"), "COMPILER_SOURCE_BYTES") + mutations = [ + (b"return upper + negative + upper + sign", b"return upper + negative + upper", "EMITTER_TARIFF"), + (b"return sign + lower + negative + lower", b"return lower + sign + negative + lower", "EMITTER_BOUNDARY"), + (b'"a" if a_cost < b_cost else "b"', b'"a" if a_cost > b_cost else "b"', "EMITTER_TARIFF"), + ] + for before, after, reason in mutations: + need(raw.count(before) == 1, "UNIQUE_SOURCE_MUTATION") + changed = load_compiler(raw.replace(before, after)) + rejected += expect_reject(lambda: check_emitter(changed, [3, 5], [2, -1], tariff), reason) + incoming = module["compile_exchange"]([1, 0], [1, 0]) + outgoing_b = module["compile_exchange"]([1, 0], [1, 1]) + leaked = literal(outgoing_b, literal(incoming, [0, 0, 1])) + need(leaked == [0, -1, 1], "MISMATCHED_B_COUNTEREXAMPLE") + outgoing_a = module["compile_exchange"]([1, 1], [1, 0]) + changed_spare = literal(outgoing_a, literal(incoming, [0, 1, 0])) + need(changed_spare == [-1, 1, 1], "MISMATCHED_A_COUNTEREXAMPLE") + ops = module["compile_exchange"]([3, 5], [2, -1]) + at_use = literal(ops, [1, 0, 7]) + at_use[-1] += 1 + logical_boundary = literal(ops, at_use) + need(at_use == [9, -4, 4] and logical_boundary == [3, -1, 7], "OBSERVER_COUNTEREXAMPLE") + huge = module["compile_exchange"]([2**63, 1], [0, 1]) + need(any(abs(q) + 1 >= 2**16 for _, _, _, q in huge), "CALLER_CAP_DISTINCTION") + invalid = [([], []), ([1], [0]), ([Q(1, 3)], [3]), ([True], [1]), + ([Q(1, 2**33)], [2**33])] + reasons = ["Matching bounded dimensions", "Dual pairing equals one", "Bounded dyadic denominator", + "Exact coefficients", "Bounded dyadic denominator"] + for (a, b), reason in zip(invalid, reasons): + rejected += expect_reject(lambda a=a, b=b: module["compile_exchange"](a, b), reason) + return {"exact_reason_rejections": rejected, "boundary_discriminators": 4, + "mismatched_column_output": list(map(str, leaked)), + "mismatched_row_output": list(map(str, changed_spare)), + "fused_after_first_use": list(map(str, at_use)), + "separate_after_first_consumer": list(map(str, logical_boundary))} + + +def main(): + raw, tariff_source = bindings() + module = load_compiler(raw) + tariff = source_tariff_expression(tariff_source) + nc = runpy.run_path(str(HERE / "noncommutative.py"))["check"]() + requests = 0 + for n in range(1, 17): + for k in range(8): + if n == 1: + a, b = [Q(2**k)], [Q(1, 2**k)] + else: + b = [Q(1)] + [Q((i + k) % 5 - 2, 2**(k % 3)) for i in range(1, n)] + a = [Q(0)] + [Q((2 * i + k) % 7 - 3, 2**((k + 1) % 3)) for i in range(1, n)] + a[0] = 1 - sum(a[i] * b[i] for i in range(1, n)) + check_emitter(module, a, b, tariff) + requests += 1 + for a, b in [([3, 5], [2, -1]), ([2**63, 1], [0, 1]), ([Q(1, 2**32)], [2**32])]: + check_emitter(module, a, b, tariff) + requests += 1 + result = {"status": "PASS_DUAL_EXCHANGE_FUSION_AUDIT", "certificate": nc, + "emitter_requests": requests, "emitter_factorizations": 3 * requests, + "functional": functional_evidence(module), "controls": controls(module, raw, tariff), + "observers": observer_evidence(module), + "source_head": SOURCE_HEAD, "source_sha256": COMPILER_SHA, + "tariff_sha256": TARIFF_SHA, + "scope": "Closed macro only; no actual P104 cut, supplier, rounded analysis or new kappa."} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() From a2d6b3920abb26f22b61b776088209e09b03590e Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Fri, 30 Oct 2026 23:40:11 +0800 Subject: [PATCH 2/2] Compile changing-dual junctions: scalar allowance 288 to 224 Compare after cancelling the baseline's adjacent sign pair; retain both outer exchanges and both inner consumers. Exact coefficient admission, prefix bounds, unfavorable-tariff control and independent nonlinear replay are included. Prepared for @CubeJerry with OpenAI Codex assistance; credit Nick Petalas, Ali Romman and retained P104 lineage. No new kappa. --- .../INDEPENDENT-TRANSITION.md | 127 +++++++++++ .../dual-exchange-independent-audit/README.md | 16 ++ .../dual-exchange-independent-audit/TASK.json | 29 ++- .../TRANSITION-PROOF.md | 207 ++++++++++++++++++ .../VERIFY.json | 54 +++++ .../independent_transition.py | 180 +++++++++++++++ .../transition.py | 49 +++++ .../verify_transition.py | 136 ++++++++++++ 8 files changed, 795 insertions(+), 3 deletions(-) create mode 100644 research/dual-exchange-independent-audit/INDEPENDENT-TRANSITION.md create mode 100644 research/dual-exchange-independent-audit/TRANSITION-PROOF.md create mode 100644 research/dual-exchange-independent-audit/independent_transition.py create mode 100644 research/dual-exchange-independent-audit/transition.py create mode 100644 research/dual-exchange-independent-audit/verify_transition.py diff --git a/research/dual-exchange-independent-audit/INDEPENDENT-TRANSITION.md b/research/dual-exchange-independent-audit/INDEPENDENT-TRANSITION.md new file mode 100644 index 0000000000..9a3f949eda --- /dev/null +++ b/research/dual-exchange-independent-audit/INDEPENDENT-TRANSITION.md @@ -0,0 +1,127 @@ +# Independent review: changing dual columns with a fixed row + +Research worker A, for @CubeJerry, with substantial OpenAI Codex assistance. +No author junction implementation was imported or read. The fixed original +PR6280 compiler is the only predecessor executable used. The module argument +below is independent of the finite scalar tests. + +## Universal module proof + +Let A:X→Z, B,D:Z→X be module homomorphisms with AB=AD=I_Z. Let K=B−D, +so AK=0. For S_B(x,z)=((I−BA)x+Bz,Ax), direct composition in chronological +order gives + + S_B ; S_D : (x,z) ↦ (x+K(z−Ax),z). + +No maps commute in this derivation. Apply L_(-A), then U_K, then L_A: + + (x,z) → (x,z−Ax) → (x+K(z−Ax),z−Ax) + → (x+K(z−Ax),z−Ax+A[x+K(z−Ax)]) + = (x+K(z−Ax),z). + +Thus the three-block junction is exact over arbitrary modules, including +nonfaithful or torsion modules. A norm or scalar tariff is an additional +source-specialization statement, not part of this module-general identity. + +For arbitrary total functions G,H:Z→Z, the fully closed sequence + + S_B;G;S_B;S_D;H;S_D + +can replace its middle two exchanges by the junction, retaining **both outer +exchanges and both inner functions**. Its data endpoint is exactly + + x + B(G(Ax)−Ax) + D(H(G(Ax))−G(Ax)), + +and the arbitrary original spare z is restored. This is generally not +F_(H∘G) for a single fixed dual column. Omitting the junction leaves the +mismatched single-exchange boundary defect and leaks the arbitrary spare. +The outer columns may differ because the junction explicitly compensates +their difference; this does not contradict the one-use matching-boundary +theorem, whose intervening operation acts only on the spare. + +Fixed A, common physical roles/chart and unchanged module meanings are +necessary hypotheses of this stated construction. Different rows require a +different formula. Observing the old returned-consumer boundary between the +removed exchanges is not licensed: the new junction returns the next encoded +state, and the old intermediate returned state is not preserved as an +observation boundary. No mutating intervention or observer/control-flow +contract is supplied. Every native, delivery, chart, ownership, precision and +recursive cost remains outside the scalar saving unless separately proved. + +## Complete named invoice and finite independent evidence + +For a=(3,5), b=(2,−1), d=(7,−4), the difference is k=(−5,3). +Under the authenticated PR5602 tariff, the coefficient totals are +A_a=26, A_b=18, A_d=28, A_k=26. The source's cheapest exchanges cost +64 and 82. The literal junction costs 2A_a+A_k=78, so the complete two-use +raw scalar allowance decreases from 2·64+2·82=292 to 64+78+82=224. +A fairer comparison first removes the obvious adjacent sign pair: the entering +exchange's last instruction and the leaving exchange's first instruction are +both SCALE(spare,−1). Their composition is identity. Deleting these two +instructions costs no assumptions and gives the sign-peepholed baseline +**288**, versus **224** for the junction, a further allowance saving of **64**. +The corresponding **emitted scalar ADD/SCALE instruction** counts are 26 +versus 20 (raw source count28). The junction count includes seven entering, +six junction and seven exiting instructions. These are not primitive +native/Boolean gate counts or an optimal-circuit claim. + +The separate checker authenticates source SHA256 and Git blob, plus the +actual caller tariff SHA256. It implements its own exact interpreter, +three-block emission and binary tariff count; it imports no author junction +code or polynomial verifier. All three input basis columns agree with both +literal source exchanges, their sign-peepholed version, and the direct endpoint. For all 125 inputs in +{-2,-1,0,1,2}³ and all 16 ordered pairs from four functions (identity, +square-plus-one, constant-minus-two, absolute-value-minus-two), all 2,000 +raw separate, sign-peepholed, junction and direct-formula endpoints agree. This finite scalar +corroboration does not replace the universal module/set-map proof above. + +Six discriminators detect reversed difference sign, omitted exit lower +block, omitted junction with dirty spare, a changed common row, the new +coefficient-cap obstruction below, and an observer reading the removed +returned-state boundary. Warning-strict normal and optimized Python produce +identical receipts. + +## Coefficient admission and magnitude limits + +Even admitted old coefficients can produce an inadmissible difference. +For a=(1,0), b=(1,65534), d=(1,−65534), both dualities hold and every old +emitted coefficient satisfies the actual caller condition |q|+1<65536. +The new difference coefficient 131068 violates it. The new three-block +junction therefore needs its own coefficient-admission check; source +compiler acceptance of both old pairs is insufficient. This explicit case +was independently supplied by worker A and relayed to the author. + +For scalar fields with the usual absolute value, a conservative prefix +bound relative to the junction entrance is + + (1+Σ|a_i|)² (1+Σ|b_i−d_i|). + +Each lower block has norm at most the first factor before squaring; every +upper-block prefix has norm at most the difference factor. The named bound +is 729. The checker computes every exact scalar-prefix row-sum norm: +4,9,46,46,129,46, so the actual maximum is 129. This establishes no global +macro magnitude/error bound: arbitrary G,H can have unbounded amplification, +and differing common charts or physical field availability remain unproved. + +## Reproduction and source pins + +Frozen prior public package: 0ff4a9f9cf763d5fa385d674fea915da53792078, +canonical scientific base 2485805a6d47f36ea83ddde6327d453ac82d44dc. +Original compiler: PR6280 4d6e4374d6fdda7df72ddeb19dd6756353383346, +blob 9ead98d5735474d1fd35b101a1f4d50426b7e943. Its author notice remains intact. + + python3 -I -W error -B research/dual-exchange-independent-audit/independent_transition.py --package research/dual-exchange-independent-audit + +Expected PASS_INDEPENDENT_CHANGING_COLUMN_JUNCTION, 2,000 nonlinear cases, +288→224 scalar allowance and26→20 emitted instructions after the trivial +SCALE-pair cancellation (raw292/28), plus six discriminators. +Add -O for identical optimized output. The checker uses only the original +source/compiler.py and the pinned external caller tariff; it neither reads +nor imports any new junction implementation. + +No blocker was found for this scoped exact endpoint and local invoice result. +No actual selected P104 interval, precision admission, physical caller, +primitive optimality or new κ is established. Credit Nick Petalas for the +source exchange, Ali Romman for the dual interface and tariff, and worker D +for the proposed changing-column contribution. This review supplies a +complementary independent derivation and verifier, not a separate result/PR. diff --git a/research/dual-exchange-independent-audit/README.md b/research/dual-exchange-independent-audit/README.md index 19bd5545e9..78c8f5479c 100644 --- a/research/dual-exchange-independent-audit/README.md +++ b/research/dual-exchange-independent-audit/README.md @@ -104,3 +104,19 @@ The source notice is preserved. New work is Apache-2.0; no literature-wide priority claim is made for retractions, conjugation or cancellation. The registered replay also includes an independent lead-review field interpreter covering all 59,049 F3 function-pair/input/emitter cases for the named nonunit pair, plus a mismatched-pair leakage control. + +## Changing dual columns: a completely priced local extension + +[TRANSITION-PROOF.md](TRANSITION-PROOF.md) gives the exact same-row junction +`S_(A,B);S_(A,D) = L_-A;U_(B-D);L_A` for `AB=AD=I`. Its source-bound named +two-consumer macro reduces scalar allowance **288→224 after cancelling the +original adjacent signs**, retaining both outer exchanges and all inner calls; +emitted ADD/SCALE instructions fall **26→20**. The raw source-emission +comparison is **292→224**, with **28→20** instructions. Difference coefficients and scalar prefixes are checked separately. +An admitted dyadic example where the tariff instead rises **132→212** makes +the local cost-comparison requirement explicit. + +[INDEPENDENT-TRANSITION.md](INDEPENDENT-TRANSITION.md) supplies a separate module +derivation and 2,000 nonlinear checks using its own construction and interpreter. +The new normal/optimized checks are registered in VERIFY.json. No actual P104 +interval, rounded-budget improvement, primitive optimum, or new κ is claimed. diff --git a/research/dual-exchange-independent-audit/TASK.json b/research/dual-exchange-independent-audit/TASK.json index 3b4965ff9c..1c6d52d46b 100644 --- a/research/dual-exchange-independent-audit/TASK.json +++ b/research/dual-exchange-independent-audit/TASK.json @@ -75,13 +75,13 @@ ] }, "scope_status": "changed", - "actual_scope": "Source-bound independent algebraic audit and safe-fusion theorem for PR6280 dual-exchange consumers, including arbitrary inner functions and exact observer/pair-matching boundaries.", + "actual_scope": "Source-bound independent algebraic audit and safe-fusion theorem for PR6280 dual-exchange consumers, including arbitrary inner functions and exact observer/pair-matching boundaries. Extension: same-row changing-dual three-shear junction with exact source tariff, coefficient admission and complete two-consumer local budget.", "scope_change_reason": "The assigned formal-interface card is narrowed to a written quantified interface proof and independent free-operator certificate for the newly published PR6280 emitter; no proof-assistant or selected-assumption discharge is claimed.", "bottleneck_link": "Repeated scalar basis preparation may be removed only within a closed consumer macro. This proves the exact local tariff and ABI boundary, while leaving actual P104 applicability and all paid native calls open.", "budget_minutes": 90, "stop_rule": "Stop after the same-pair composition theorem, arbitrary-spare boundary characterization, and source-bound controls; do not launch a physical cut search or claim supplier admission.", "outcome": "completed", - "evidence": "PROOF.md; verify.py and noncommutative.py; normal/optimized registered checks. Exact predecessor in ORIGIN.json.", + "evidence": "PROOF.md; verify.py and noncommutative.py; normal/optimized registered checks. Exact predecessor in ORIGIN.json. TRANSITION-PROOF.md, verify_transition.py, INDEPENDENT-TRANSITION.md and independent_transition.py.", "author": "@CubeJerry with OpenAI Codex assistance", "ai_assistance": "Substantial OpenAI Codex assistance, including exchange-audit subagent construction and separate adversarial proof review; no independent human or formal-kernel acceptance. Research worker A independently derived and checked the exact invariant-observer class and its reachability limitation.", "open_questions": [ @@ -106,5 +106,28 @@ "rounded prefix amplification, deferred" ] }, - "overlap_coverage": "Root checked live PR bodies and bounded all-state exchange/nonlinear searches; narrow main README search found the distinct p104-joint-compensation precedent. Discussion posting unavailable; no exhaustive novelty claim." + "overlap_coverage": "Root checked live PR bodies and bounded all-state exchange/nonlinear searches; narrow main README search found the distinct p104-joint-compensation precedent. Discussion posting unavailable; no exhaustive novelty claim.", + "extension": { + "track_seed": 28, + "track": "complex supplier", + "scientific_base": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "owned_object": "S_(A,B);S_(A,D) with AB=AD=I in one unchanged physical chart", + "selected_candidate": "changing dual columns with fixed row", + "deferred_candidates": [ + "transpose changing rows", + "general changing pairs" + ], + "budget_minutes": 20, + "stop_rule": "One valid, completely priced source-bound local improvement or unfavorable complete local budget; no broad circuit search.", + "outcome": "Complete local allowance 288\u2192224 after obvious adjacent-sign cancellation (raw 292\u2192224), with every consumer retained; separate unfavorable 132\u2192212 case prevents a uniform saving claim.", + "independent_review": "Worker A derived the module identity and constructed a separate source-bound interpreter without importing or reading the author transition code.", + "open_obligations": [ + "Actual selected caller interval and physical role/chart admission", + "Compatibility of any removed observation boundary", + "New rounded-prefix error admission if used numerically", + "Complete physical supplier and recursive cost accounting" + ], + "no_new_kappa": true, + "published_predecessor": "0ff4a9f9cf763d5fa385d674fea915da53792078" + } } diff --git a/research/dual-exchange-independent-audit/TRANSITION-PROOF.md b/research/dual-exchange-independent-audit/TRANSITION-PROOF.md new file mode 100644 index 0000000000..ee97c81dad --- /dev/null +++ b/research/dual-exchange-independent-audit/TRANSITION-PROOF.md @@ -0,0 +1,207 @@ +# A paid junction for changing dual columns + +This extends the same-pair cancellation theorem to two different dual columns +with one fixed row and physical chart. It supplies a concrete local scalar +saving, not a physical P104 installation, a rounding-budget improvement, an +unrestricted circuit optimum, or a new multiplication exponent. **No new κ.** + +## Quantified identity and emitted program + +Let X,Y be modules, A:X→Y and B,D:Y→X be linear maps with AB=AD=I_Y. All +compositions below are typed; no commutation or coordinate scalar assumption +is needed for the identity. Put E=B−D, so AE=0. With + +``` +S_B(x,z) = (x+B(z−Ax), Ax), +``` + +chronological application of S_B then S_D gives + +``` +R(x,z) = S_D(S_B(x,z)) = (x+E(z−Ax), z). +``` + +Indeed A(x+B(z−Ax))=z. The second exchange therefore subtracts D(z−Ax) +from the data and returns z to the spare. The following chronological three +shears implement R on arbitrary data and arbitrary dirty spare: + +``` +L_-A: z ← z−Ax +U_E: x ← x+Ez +L_A: z ← z+Ax. +``` + +The last spare value is z_original−Ax_original+A(x_original+E(z_original−Ax_original)) +=z_original because AE=0. This also proves exact data restoration when B=D; +`compile_transition` emits the empty program in that case. + +The standalone junction restores its spare but its data generally depend on +that arbitrary spare, exactly as the literal two exchanges do. This is an +internal representation; the dependence disappears only in the complete, +correctly paired outer macro below. It does not contradict PROOF.md's +matching-boundary theorem, which demanded a closed consumer with no dirty-spare +dependence in its data endpoint. + +For a scalar row a and columns b,d of common dimension n, `transition.py` +emits the lower ADDs in increasing data-role order, the upper ADDs in increasing +role order, then the final lower ADDs. Within each lower block the data are +unchanged; within the upper block the spare is unchanged. Hence the scalar +sequence implements the three displayed block shears exactly. Every ADD uses +distinct source and target roles. No helper, initialization, erasure, copied +source, extra consumer invocation, or sign SCALE is introduced. + +## Complete local macro, not just an endpoint tariff + +Consider two closed consumers in one unchanged chart and ownership state: + +``` +S_B; G1_on_spare; S_B; S_D; G2_on_spare; S_D. +``` + +Replace only the consecutive middle two exchanges by R. All outer exchanges +and both consumers remain. This is valid for arbitrary functions G1,G2 on Y, +since the junction identity holds on every incoming state. In particular, +writing w0=Ax, w1=G1(w0), w2=G2(w1), the complete output is + +``` +(x+B(w1−w0)+D(w2−w1), z). +``` + +For k consumers with one fixed A and columns B_i, the same induction gives +`(x+Σ_i B_i(w_i−w_(i−1)),z)` and an allowance comprising the first and last +outer exchange, each chosen interior junction, and every paid consumer call. +This is an accounting identity, not a claim that all junctions are cheaper. + +There must be no externally visible observation, modification, native call, +frame transition, ownership transition, or source-access obligation *inside* +the replaced junction. In particular, the intermediate state after the first +of its original exchanges is generally not preserved. Any permission for an +observer requires its own established invariant; this construction supplies +none. Chart preparation and all required work outside the junction remain +paid. Existing rounded/conditioned interfaces do not inherit a better error +budget merely from this exact endpoint equality. + +## Source-bound scalar allowance and a concrete saving + +The frozen PR6280 emitter is head +`4d6e4374d6fdda7df72ddeb19dd6756353383346`, authenticated through ORIGIN.json +and SHA256 `9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf`. +The actual PR5602 caller tariff and coefficient admission are in canonical +`research/p104-coupled-helper-bases/local.py`, SHA256 +`5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925`, at base +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The earlier published +independent audit package is commit `0ff4a9f9cf763d5fa385d674fea915da53792078`; +this extension retains its source pins. + +Let c(v) be the sum of the source's nonzero ADD tariffs for vector v. The +source's cheapest of its two exchange factorizations costs +`B_v=2+c(a)+c(v)+min(c(a),c(v))`. A nonzero transition costs exactly +`J=2c(a)+c(b−d)` and has `2 nnz(a)+nnz(b−d)` scalar ADDs. For zero difference +J=0 and there are no operations. The complete two-consumer comparison is + +``` +old: 2(B_b+B_d) + cost(G1)+cost(G2) +new: B_b+J+B_d + cost(G1)+cost(G2). +``` + +For `a=(3,5), b=(2,−1), d=(7,−4)`, both pairings equal one, +`E=(−5,3)`, and exact source pricing gives: + +| Quantity | Value | +|---|---:| +|c(a), c(b), c(d), c(E)|26, 18, 28, 26| +|B_b, B_d, J|64, 82, 78| +|Junction allowance before → after|146 → 78| +|Complete macro allowance before → after|292 → 224| +|Complete macro scalar ADD/SCALE instructions before → after|28 → 20| +|Complete allowance after cancelling adjacent original signs → replacement|288 → 224| +|Instructions after cancelling adjacent original signs → replacement|26 → 20| + +The scientifically stronger comparison first performs the obvious source +peephole: the last instruction of the inner S_B and the first instruction of +the inner S_D are both `SCALE(spare,spare,-1)`, so they cancel. The verifier +checks those exact emitted operations, removes precisely those two operations, +and compares every input basis column with both the raw and replacement +junctions. This reduced baseline costs 288 with 26 instructions. **The +replacement therefore saves 64 scalar allowance units even after the obvious +sign cancellation, reducing 288→224 and 26→20 instructions.** + +The raw source-emission comparison remains 292→224, saving 68 units and +28→20 instructions. Both comparisons retain all inner work and both outer +exchanges. Neither baseline is claimed to be the globally cheapest circuit. +The instruction counts are not primitive native or Boolean gate counts. + +The rewrite is not uniformly cheaper. For `a=(1,0), b=(1,1), d=(1,2^-32)`, +the difference `1−2^-32` has a dense numerator: the literal two-exchange tariff +is 132 but the three-shear tariff is 212. The verifier reproduces both valid +endpoints and this unfavorable comparison. Callers must compare complete +admissible local budgets rather than selecting the three-shear form blindly. +No search over arbitrary circuits was conducted. + +## Admission and scalar-prefix control + +Inputs satisfy the source compiler's exact dyadic interface: dimension at most +16, numerator magnitude at most 64 bits, denominator a power of two with at +most 33 bits, and both exact dual pairings. The difference is checked against +these bounds separately; subtraction can increase numerator size. A separate +control uses `a=(1,0), b=(1,2^64−1), d=(1,−(2^64−1))`: both old pairs +pass the compiler interface, but E has a 65-bit numerator and is rejected +before the physical-growth check. This example concerns compiler admission, +not admission by the stricter physical caller. + +The actual physical caller additionally requires `|q|+1<2^16` for every scalar +coefficient. The new compiler checks that condition for every emitted a and E +coefficient. This does not assert that arbitrary input b and d satisfy that +physical caller: the verifier separately checks every actual baseline +coefficient for the compared fixtures. For example, `a=(1,0), b=(1,65534), +d=(1,−65534)` consists of individually caller-admitted pairs, yet its difference +131068 fails the caller's growth admission. The replacement is rejected; +the source's admission is not widened. When E=0 no scalar coefficient is emitted. + +Write α=1+Σ|a_i| and ε=1+Σ|E_i|. Every partial scalar lower block has infinity +operator norm at most α, and every partial upper block at most ε. Therefore +every scalar prefix of the replacement has amplification at most `α² ε`. +This bound includes the partial restoration block, which cannot be ignored. +For the named fixture α=ε=9, so the bound is 729; exact coefficient-row replay +finds actual maximum 129, the same as the original cheapest two-exchange +junction. In the final lower block a partial spare row is `(45,70,−14)`, whose +absolute row sum is 129, before the final spare returns to its input value. +The separate scalar-section bounds compose with whatever amplification +contracts the unchanged G_i actually provide. No uniform bound is asserted +for arbitrary nonlinear functions, and no unchanged rounded budget is claimed. + +## Reproduction, review, and limits + +```sh +python3 -I -W error -B research/dual-exchange-independent-audit/verify_transition.py +python3 -I -W error -B -O research/dual-exchange-independent-audit/verify_transition.py +``` + +Expected receipt: `PASS_SOURCE_BOUND_CHANGING_DUAL_TRANSITION`, complete +allowance `288→224` after adjacent-sign cancellation (`292→224` raw), +instructions `26→20` (`28→20` raw), and eight rejection/discrimination +controls. The checker authenticates source bytes before execution, extracts +the actual tariff expression, checks six exact fixtures through all nine +pairs of source emitter modes (54 comparisons), checks 125 arbitrary-spare +states, and compares 375 complete nonlinear macros with direct substitution. +Fixture dimensions include 1, 2, 3 and the maximum 16; dyadic coefficients, +zero differences and an unfavorable tariff are included. The fixed fixture +suite is corroboration of the all-module proof, not a universal finite search. +Track seed 28 selects the task; no random seed is used. The stopping rule is +one valid completely priced source-bound improvement, not circuit optimization. + +Negative controls cover false duality, coefficient-cap and difference-numerator +overflow, nondyadic and +inexact input, missing restoration, reversed transition direction, and an +observation at an eliminated boundary. No P104 caller interval is installed; +source and chart admission, observational compatibility, native costs, recursive +interfaces and any rounded implementation still require actual-caller proof. +The selected κ and all five inherited framework assumptions are unchanged. + +Credit Nick Petalas for the PR6280 exchange compiler and Ali Romman for the +retained PR5602 tariff caller, with the earlier audit's full construction lineage +unchanged. Jerry Chen, @CubeJerry; substantial OpenAI Codex assistance from +worker D (construction and source-bound verifier), the lead (junction proposal +and independent coefficient-prefix check), and worker A (independent universal +identity and complete-cost review). Independent human/formal-kernel acceptance +is not claimed. diff --git a/research/dual-exchange-independent-audit/VERIFY.json b/research/dual-exchange-independent-audit/VERIFY.json index 33b7340929..4b134bfdec 100644 --- a/research/dual-exchange-independent-audit/VERIFY.json +++ b/research/dual-exchange-independent-audit/VERIFY.json @@ -56,6 +56,60 @@ ], "timeout_seconds": 60, "checks": "Independent exhaustive F3 function-pair composition:59049 cases across all source emitter modes and mismatched-pair leakage control." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify_transition.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound changing-dual transition, full 288-to-224 macro allowance after exact source-sign cancellation (292-to-224 raw), scalar-prefix and coefficient-cap checks, nonlinear dirty-state evidence, eight controls and unfavorable-tariff discriminator." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify_transition.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound changing-dual transition, full 288-to-224 macro allowance after exact source-sign cancellation (292-to-224 raw), scalar-prefix and coefficient-cap checks, nonlinear dirty-state evidence, eight controls and unfavorable-tariff discriminator." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_transition.py", + "--package", + "{package}" + ], + "timeout_seconds": 60, + "checks": "Independent module proof corroboration and separate transition construction/interpreter: 2000 nonlinear cases, exact source tariff, six boundary/cap discriminators." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/independent_transition.py", + "--package", + "{package}" + ], + "timeout_seconds": 60, + "checks": "Independent module proof corroboration and separate transition construction/interpreter: 2000 nonlinear cases, exact source tariff, six boundary/cap discriminators." } ] } diff --git a/research/dual-exchange-independent-audit/independent_transition.py b/research/dual-exchange-independent-audit/independent_transition.py new file mode 100644 index 0000000000..853b1e1e66 --- /dev/null +++ b/research/dual-exchange-independent-audit/independent_transition.py @@ -0,0 +1,180 @@ +"""Independent changing-column junction audit, with no author-junction imports. + +Jerry Chen (@CubeJerry), with OpenAI Codex assistance (research worker A). +Nick Petalas retains the authenticated PR6280 source emitter; Ali Romman the +PR5602 scalar tariff. New checker material is Apache-2.0. +""" +from fractions import Fraction as F +from hashlib import sha1, sha256 +from itertools import product +from pathlib import Path +import argparse +import json + +EMITTER_SHA = '9d7b71ed4da90360f8a0f15b7a89599340efbb4eb1ff40054e11e621f85df5bf' +EMITTER_BLOB = '9ead98d5735474d1fd35b101a1f4d50426b7e943' +TARIFF_SHA = '5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925' + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def source(package): + raw = (package / 'source/compiler.py').read_bytes() + need(sha256(raw).hexdigest() == EMITTER_SHA, 'SOURCE_SHA') + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + == EMITTER_BLOB, 'SOURCE_BLOB') + tariff = package.parents[1] / 'research/p104-coupled-helper-bases/local.py' + need(sha256(tariff.read_bytes()).hexdigest() == TARIFF_SHA, 'TARIFF_SHA') + namespace = {'__name__': 'authenticated_source_compiler'} + exec(compile(raw, 'authenticated_source_compiler.py', 'exec'), namespace) + return namespace['compile_exchange'] + + +def execute(ops, state): + state = list(map(F, state)) + for name, destination, origin, coefficient in ops: + need(type(destination) is int and type(origin) is int + and 0 <= destination < len(state) and 0 <= origin < len(state), 'ROLES') + if name == 'ADD': + need(destination != origin, 'DISTINCT_ROLES') + state[destination] += coefficient * state[origin] + else: + need(name == 'SCALE' and destination == origin and coefficient == -1, + 'SIGN_ONLY') + state[destination] *= coefficient + return state + + +def price_coefficient(q): + q = F(q) + n, d = abs(q.numerator), q.denominator + need(n > 0, 'NONZERO_PRICE') + bits, ones, halves = 0, 0, 0 + while n: + n, digit = divmod(n, 2) + bits += 1 + ones += digit + while d > 1: + d, rem = divmod(d, 2) + need(rem == 0, 'DYADIC_PRICE') + halves += 1 + return 2 * (2 + bits + ones + halves) + + +def price(ops): + return sum(2 if name == 'SCALE' else price_coefficient(q) + for name, _, _, q in ops) + + +def junction(a, b, d): + a, b, d = (list(map(F, row)) for row in (a, b, d)) + need(len(a) == len(b) == len(d) > 0, 'DIMENSIONS') + need(sum(x * y for x, y in zip(a, b)) == + sum(x * y for x, y in zip(a, d)) == 1, 'DUAL_PAIR') + n = len(a) + lower = [('ADD', n, i, q) for i, q in enumerate(a) if q] + upper = [('ADD', i, n, x - y) for i, (x, y) in enumerate(zip(b, d)) if x != y] + negative = [(name, dst, src, -q) for name, dst, src, q in lower] + return negative + upper + lower + + +def target(a, b, d, state): + delta = state[-1] - sum(x * y for x, y in zip(a, state[:-1])) + return [x + (left - right) * delta + for x, left, right in zip(state[:-1], b, d)] + [state[-1]] + + +def columns(ops, width): + return [execute(ops, [int(i == j) for i in range(width)]) for j in range(width)] + + +def nonlinear_macro(enter, leave, transition, state, first, second, separate): + state = execute(enter, state) + state[-1] = first(state[-1]) + state = execute(enter + leave if separate else transition, state) + state[-1] = second(state[-1]) + return execute(leave, state) + + +def coefficient_cap(ops): + return all(abs(q) + 1 < 2 ** 16 for _, _, _, q in ops) + + +def check(package): + emit = source(package) + a, b, d = [F(3), F(5)], [F(2), F(-1)], [F(7), F(-4)] + entering, leaving, transition = emit(a, b), emit(a, d), junction(a, b, d) + expected = [target(a, b, d, [F(i == j) for i in range(3)]) for j in range(3)] + need(entering[-1] == leaving[0] == ('SCALE', 2, 2, F(-1)), + 'ADJACENT_SIGN_PEEPHOLE') + peepholed = entering[:-1] + leaving[1:] + need(columns(peepholed, 3) == expected, 'PEEPHOLED_ALL_INPUT_COLUMNS') + need(price(peepholed) == 142 and len(peepholed) == 12, 'PEEPHOLED_TARIFF') + need(columns(entering + leaving, 3) == columns(transition, 3) == expected, + 'ALL_INPUT_COLUMNS') + need((price(entering), price(leaving), price(transition)) == (64, 82, 78), 'TARIFF') + need((len(entering), len(leaving), len(transition)) == (7, 7, 6), 'INSTRUCTIONS') + need(coefficient_cap(entering + leaving + transition), 'NAMED_CAP') + prefix_norms = [] + for length in range(1, len(transition) + 1): + cols = columns(transition[:length], 3) + prefix_norms.append(max(sum(abs(col[i]) for col in cols) for i in range(3))) + envelope = (1 + sum(map(abs, a))) ** 2 * (1 + sum(abs(x - y) for x, y in zip(b, d))) + need(max(prefix_norms) == 129 and envelope == 729, 'PREFIX_ENVELOPE') + functions = (lambda t: t, lambda t: t * t + 1, lambda t: F(-2), lambda t: abs(t) - 2) + count = 0 + for state in product(range(-2, 3), repeat=3): + for first, second in product(functions, repeat=2): + literal = nonlinear_macro(entering, leaving, transition, state, first, second, True) + replaced = nonlinear_macro(entering, leaving, transition, state, first, second, False) + cleaned = nonlinear_macro(entering, leaving, peepholed, state, first, second, False) + ax = sum(q * x for q, x in zip(a, state[:-1])) + gx, hgx = first(ax), second(first(ax)) + direct = [x + bv * (gx - ax) + dv * (hgx - gx) + for x, bv, dv in zip(state[:-1], b, d)] + [F(state[-1])] + need(literal == cleaned == replaced == direct, 'NONLINEAR_MACRO') + count += 1 + reverse = junction(a, d, b) + need(columns(reverse, 3) != expected, 'SIGN_CONTROL') + need(columns(transition[:-2], 3) != expected, 'EXIT_LOWER_CONTROL') + identity = lambda t: t + state = [F(0), F(0), F(1)] + good = nonlinear_macro(entering, leaving, transition, state, identity, identity, False) + omitted = nonlinear_macro(entering, leaving, [], state, identity, identity, False) + need(good == state and omitted == [F(-5), F(3), F(1)], 'MISSING_JUNCTION_LEAK') + different_row = emit([1, 0], [1, 0]) + emit([1, 1], [1, 0]) + need(execute(different_row, [0, 1, 0]) == [-1, 1, 1], 'COMMON_ROW_CONTROL') + cap_a, cap_b, cap_d = [1, 0], [1, 65534], [1, -65534] + old = emit(cap_a, cap_b) + emit(cap_a, cap_d) + new = junction(cap_a, cap_b, cap_d) + need(coefficient_cap(old) and not coefficient_cap(new), 'DIFFERENCE_CAP_GAP') + # A caller observing the intermediate restored state distinguishes the new prefix. + encoded = execute(entering, [1, 0, 7]) + encoded[-1] += 1 + returned = execute(entering, encoded) + after_new_junction = execute(transition, encoded) + need(returned[-1] != after_new_junction[-1], 'INTERMEDIATE_OBSERVER_CONTROL') + return {'status': 'PASS_INDEPENDENT_CHANGING_COLUMN_JUNCTION', + 'source_sha256': EMITTER_SHA, 'tariff_sha256': TARIFF_SHA, + 'linear_input_columns': 3, 'nonlinear_cases': count, + 'complete_two_use_scalar_allowance': {'raw_separate': 292, 'sign_peepholed': 288, 'junction': 224}, + 'complete_two_use_scalar_instructions': {'raw_separate': 28, 'sign_peepholed': 26, 'junction': 20}, + 'allowance_saved_against_sign_peephole': 64, + 'junction_allowance': 78, 'junction_prefix_norms': list(map(str, prefix_norms)), + 'junction_relative_prefix_bound': str(envelope), + 'named_coefficients_admitted_by_cap': True, 'scope_discriminators': 6, + 'scope': 'Exact endpoints only; same row/roles/chart; no observer or precision admission.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--package', type=Path, required=True) + args = parser.parse_args() + print(json.dumps(check(args.package.resolve()), indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/dual-exchange-independent-audit/transition.py b/research/dual-exchange-independent-audit/transition.py new file mode 100644 index 0000000000..a0a7948e84 --- /dev/null +++ b/research/dual-exchange-independent-audit/transition.py @@ -0,0 +1,49 @@ +"""Changing-dual junction in one physical chart, Apache-2.0. + +Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance. This emits +scalar ADD operations only; it does not install a physical supplier. +""" +from fractions import Fraction as Q + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def exact_vector(v): + need(type(v) in (tuple, list), 'VECTOR_CONTAINER') + need(1 <= len(v) <= 16, 'DIMENSION_BOUND') + need(all(type(q) in (int, Q) for q in v), 'EXACT_COEFFICIENTS') + v = tuple(map(Q, v)) + for q in v: + need(abs(q.numerator).bit_length() <= 64, 'NUMERATOR_BOUND') + d = q.denominator + need(d.bit_length() <= 33 and d & (d-1) == 0, 'DYADIC_DENOMINATOR') + return v + + +def compile_transition(a, b, d): + """Replace chronological S_(a,b);S_(a,d) by L_-a;U_(b-d);L_a. + + AB=AD=1 is required. Arbitrary spare input is restored at the endpoint. + Every emitted coefficient obeys PR5602's |q|+1 < 2**16 growth admission. + Inputs obey PR6280's bounded exact dyadic public interface. No claim is + made that this program minimizes cost, or that each input exchange is + itself admitted by the stricter PR5602 physical caller. + """ + a, b, d = map(exact_vector, (a, b, d)) + need(len(a) == len(b) == len(d), 'MATCHING_DIMENSIONS') + need(sum(x*y for x,y in zip(a,b)) == 1, 'FIRST_DUALITY') + need(sum(x*y for x,y in zip(a,d)) == 1, 'SECOND_DUALITY') + e = tuple(x-y for x,y in zip(b,d)) + if not any(e): + return [] + # Subtraction can exceed either public bit bounds or the physical scalar + # growth admission even though both input exchanges are individually valid. + exact_vector(e) + need(all(abs(q)+1 < 2**16 for q in (*a,*e)), 'EMITTED_SOURCE_GROWTH') + spare = len(a) + lower = [('ADD',spare,i,q) for i,q in enumerate(a) if q] + upper = [('ADD',i,spare,q) for i,q in enumerate(e) if q] + return [(op,r,s,-q) for op,r,s,q in lower] + upper + lower diff --git a/research/dual-exchange-independent-audit/verify_transition.py b/research/dual-exchange-independent-audit/verify_transition.py new file mode 100644 index 0000000000..85f8c5ed74 --- /dev/null +++ b/research/dual-exchange-independent-audit/verify_transition.py @@ -0,0 +1,136 @@ +"""Source-bound transition verification; no predecessor verifier is executed. + +@CubeJerry with OpenAI Codex assistance; Apache-2.0. +""" +from fractions import Fraction as Q +from itertools import product +from pathlib import Path +import json +import runpy + +HERE=Path(__file__).resolve().parent +# Reuse only our independent source authentication, scalar interpreter and +# tariff extraction. This module does not execute the predecessor verifier. +V=runpy.run_path(str(HERE/'verify.py')) +T=runpy.run_path(str(HERE/'transition.py')) +need=V['need'];literal=V['literal'];price=V['price'] +compile_transition=T['compile_transition'] + + +def prefix(ops,n): + columns=[[Q(i==j) for i in range(n+1)] for j in range(n+1)] + largest=Q(1) + for step in ops: + columns=[literal([step],v) for v in columns] + largest=max(largest,max(sum(abs(v[i]) for v in columns) for i in range(n+1))) + return largest,columns + + +def direct(a,b,d,values): + x,z=values[:-1],values[-1] + residual=z-sum(q*v for q,v in zip(a,x)) + return [v+(q-r)*residual for v,q,r in zip(x,b,d)]+[z] + + +def macro(first,last,junction,state,functions): + x=literal(first,state) + x[-1]=functions[0](x[-1]) + x=literal(junction,x) + x[-1]=functions[1](x[-1]) + return literal(last,x) + + +def main(): + raw,tariff_raw=V['bindings']();compiler=V['load_compiler'](raw) + tariff=V['source_tariff_expression'](tariff_raw) + # This is an additional source obligation beyond the numeric ADD tariff. + need(b"need(abs(q)+1 < 2**16, 'Fixed scalar growth bound')" in tariff_raw,'PINNED_GROWTH_ADMISSION') + fixtures=[((1,),(1,),(1,)),((3,5),(2,-1),(7,-4)),((1,0),(1,2),(1,-3)), + ((Q(1,2),Q(1,4)),(2,0),(1,2)),((1,0,0),(1,2,-1),(1,0,3)), + ((1,)+(0,)*15,(1,)+(1,)*15,(1,)+(-1,)*15)] + checks=0 + for a,b,d in fixtures: + compiler['pair'](a,b);compiler['pair'](a,d) + ops=compile_transition(a,b,d) + e=[Q(x)-Q(y) for x,y in zip(b,d)] + expected=0 if not any(e) else 2*sum(V['price_coefficient'](x) for x in a if x)+sum(V['price_coefficient'](x) for x in e if x) + need(price(ops)==expected==compiler['allowance'](ops),'TRANSITION_TARIFF') + for op,r,s,q in ops: + need(op=='ADD' and r!=s and abs(q)+1<2**16,'EMITTED_SOURCE_ADMISSION') + need(eval(tariff,{'__builtins__':{}},{'n':abs(q.numerator),'d':q.denominator})==V['price_coefficient'](q),'ACTUAL_SOURCE_TARIFF') + bound=(1+sum(map(abs,a)))**2*(1+sum(map(abs,e))) + peak,columns=prefix(ops,len(a));need(peak<=bound,'SCALAR_PREFIX_BOUND') + for mode1,mode2 in product(('a','b','cheapest'),repeat=2): + left=compiler['compile_exchange'](a,b,mode1)+compiler['compile_exchange'](a,d,mode2) + need(all(abs(q)+1<2**16 for _,_,_,q in left),'BASELINE_SOURCE_ADMISSION') + _,old_columns=prefix(left,len(a)) + need(columns==old_columns,'SOURCE_JUNCTION_COLUMNS') + for j,column in enumerate(columns): + state=[Q(i==j) for i in range(len(a)+1)] + need(column==direct(a,b,d,state),'DIRECT_JUNCTION_COLUMNS') + checks+=1 + a,b,d=fixtures[1];first=compiler['compile_exchange'](a,b);last=compiler['compile_exchange'](a,d) + junction=compile_transition(a,b,d);old=first+last + function_pairs=((lambda x:x*x+1,lambda x:abs(x)-2),(lambda x:Q(3),lambda x:x*x-x),(lambda x:-x,lambda x:x+Q(1,2))) + cases=0 + for state in product(range(-2,3),repeat=3): + need(literal(junction,state)==literal(old,state)==direct(a,b,d,state),'DIRTY_JUNCTION') + for functions in function_pairs: + before=macro(first,last,old,state,functions) + after=macro(first,last,junction,state,functions) + # Independently apply the two closed nonlinear consumers on data. + x=list(map(Q,state));z=x[-1] + for column,fn in zip((b,d),functions): + ax=sum(q*v for q,v in zip(a,x[:-1]));delta=fn(ax)-ax + x=[v+q*delta for v,q in zip(x[:-1],column)]+[z] + need(before==after==x,'COMPLETE_NONLINEAR_MACRO') + cases+=1 + need((price(first),price(last),price(junction))==(64,82,78),'NAMED_ALLOWANCES') + full_old=first+old+last;full_new=first+junction+last + need((price(full_old),price(full_new),len(full_old),len(full_new))==(292,224,28,20),'COMPLETE_LOCAL_BUDGET') + # Compare also against the immediate source peephole: the final sign of + # S_b and the initial sign of S_d are adjacent inverse operations. + sign=('SCALE',len(a),len(a),Q(-1)) + need(first[-1]==last[0]==sign,'ADJACENT_SOURCE_SIGNS') + reduced_junction=first[:-1]+last[1:] + need(prefix(reduced_junction,2)[1]==prefix(old,2)[1]==prefix(junction,2)[1], + 'SIGN_CANCELLED_ALL_COLUMNS') + reduced_full=first+reduced_junction+last + need((price(reduced_junction),price(reduced_full),len(reduced_full))==(142,288,26), + 'SIGN_CANCELLED_COMPLETE_BUDGET') + for large_column in ((1,2**64-1),(1,-(2**64-1))): + compiler['pair']((1,0),large_column) + controls=0 + for call,reason in [ + (lambda:compile_transition((3,5),(2,-1),(7,-3)),'SECOND_DUALITY'), + (lambda:compile_transition((1,0),(1,65534),(1,-65534)),'EMITTED_SOURCE_GROWTH'), + (lambda:compile_transition((1,0),(1,2**64-1),(1,-(2**64-1))),'NUMERATOR_BOUND'), + (lambda:compile_transition((1,Q(1,3)),(1,0),(1,0)),'DYADIC_DENOMINATOR'), + (lambda:compile_transition((True,0),(1,0),(1,0)),'EXACT_COEFFICIENTS')]: + controls+=V['expect_reject'](call,reason) + # Concrete semantic controls: missing restoration and reversed E sign. + need(literal(junction[:-2],[1,0,7])!=direct(a,b,d,[1,0,7]),'MISSING_RESTORATION_CONTROL') + reverse=compile_transition(a,d,b) + need(literal(reverse,[1,0,7])!=direct(a,b,d,[1,0,7]),'REVERSED_TRANSITION_CONTROL') + # An observation at the eliminated restored-spare boundary is not preserved. + state=[Q(1),Q(0),Q(7)];inner=literal(first,state);inner[-1]+=1 + boundary=literal(first,inner) + need(boundary[-1]!=inner[-1],'ELIMINATED_BOUNDARY_OBSERVER_CONTROL') + need(compile_transition(a,b,b)==[],'EMPTY_DIFFERENCE') + # A dyadic borrow can make the difference expensive despite small magnitude. + ua,ub,ud=(1,0),(1,1),(1,Q(1,2**32)) + unfavorable_old=compiler['compile_exchange'](ua,ub)+compiler['compile_exchange'](ua,ud) + unfavorable_new=compile_transition(ua,ub,ud) + need((price(unfavorable_old),price(unfavorable_new))==(132,212),'UNFAVORABLE_TARIFF_DISCRIMINATOR') + need(prefix(unfavorable_old,2)[1]==prefix(unfavorable_new,2)[1],'UNFAVORABLE_VALID_ENDPOINT') + return {'status':'PASS_SOURCE_BOUND_CHANGING_DUAL_TRANSITION','base_commit':'2485805a6d47f36ea83ddde6327d453ac82d44dc','source_head':V['SOURCE_HEAD'], + 'fixture_count':len(fixtures),'source_factorization_pairs':checks,'dirty_junction_states':125,'complete_nonlinear_macro_cases':cases, + 'named_case':{'a':list(a),'b':list(b),'d':list(d),'junction_allowance_before':price(old),'junction_allowance_after':price(junction), + 'complete_allowance_before':price(full_old),'complete_allowance_after':price(full_new),'complete_scalar_gates_before':len(full_old),'complete_scalar_gates_after':len(full_new), + 'sign_cancelled_complete_allowance_before':price(reduced_full),'sign_cancelled_complete_instructions_before':len(reduced_full), + 'saving_against_sign_cancelled_baseline':price(reduced_full)-price(full_new),'saving_against_literal_baseline':price(full_old)-price(full_new), + 'both_inner_calls_retained':True,'junction_prefix_before':str(prefix(old,2)[0]),'junction_prefix_after':str(prefix(junction,2)[0]),'junction_prefix_envelope':729}, + 'unfavorable_tariff_discriminator':{'two_exchanges':132,'three_shears':212}, + 'negative_controls':controls+3,'no_new_kappa':True} + +if __name__=='__main__':print(json.dumps(main(),sort_keys=True,indent=2))