From 19e8f0452c09cbfe99511ea697fa239c1f457314 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 17:48:04 +0300 Subject: [PATCH 1/2] All-width certificate for the complete #5413 caller: group-algebra lifting lemma, 896 port identities, free body, abelian controller (no new kappa) Co-Authored-By: Claude Fable 5.1 --- research/allwidth-caller-certificate/PROOF.md | 101 +++ .../allwidth-caller-certificate/README.md | 61 ++ .../allwidth-caller-certificate/RESULT.json | 65 ++ .../allwidth-caller-certificate/SOURCES.json | 66 ++ .../allwidth-caller-certificate/TASK.json | 95 +++ .../allwidth-caller-certificate/VERIFY.json | 38 ++ .../test_verify.py | 99 +++ .../allwidth-caller-certificate/verify.py | 580 ++++++++++++++++++ 8 files changed, 1105 insertions(+) create mode 100644 research/allwidth-caller-certificate/PROOF.md create mode 100644 research/allwidth-caller-certificate/README.md create mode 100644 research/allwidth-caller-certificate/RESULT.json create mode 100644 research/allwidth-caller-certificate/SOURCES.json create mode 100644 research/allwidth-caller-certificate/TASK.json create mode 100644 research/allwidth-caller-certificate/VERIFY.json create mode 100644 research/allwidth-caller-certificate/test_verify.py create mode 100644 research/allwidth-caller-certificate/verify.py diff --git a/research/allwidth-caller-certificate/PROOF.md b/research/allwidth-caller-certificate/PROOF.md new file mode 100644 index 0000000000..75ff6527c0 --- /dev/null +++ b/research/allwidth-caller-certificate/PROOF.md @@ -0,0 +1,101 @@ +# A lifting lemma and its certificate for the selected caller + +Mark (Matarener), with substantial Claude Code assistance. Apache-2.0. No new κ. + +## 1. Setting + +Fix a finite group `G` of exact complex matrices on `D = 2^n` coordinates. Here `G` is the dyadic Clifford group of +nine (locally) or 145 (globally) binary axes with its absolute phase, so the central scalars `i^k I` are elements +of `G`. A scalar register program with fixed coefficients evaluates, at column multiplicity `f`, to an operator +whose entries are finite sums + + A_f = sum_g c_g g^{(x) f}, c_g in C fixed, independent of f. + +The native operators enter only through `g^{(x) f}`; the coefficients `c_g` of ADD and SCALE instructions stay +outside the tensor power. This is the free-word evaluation convention of the selected proof review (#4359 +`PROOF-REVIEW.md` section 2) and of PR5376. + +## 2. Lemma + +**Lemma.** For `a = sum_g c_g g` in `C[G]`, the operators `A_f = sum_g c_g g^{(x) f}` vanish for every positive +integer `f` if and only if `a = 0` in `C[G]`. + +*Proof.* The map `rho_f: g -> g^{(x) f}` is a group homomorphism `G -> GL(D^f)`, because +`(gh)^{(x) f} = g^{(x) f} h^{(x) f}`. Its linear extension to `C[G]` is an algebra homomorphism, so `a = 0` +implies `A_f = rho_f(a) = 0` for every `f`. Conversely suppose `rho_f(a) = 0` for all `f >= 1`. Let `rho = rho_1`, +which is faithful because `G` is a group of matrices. The representation `rho (x) R`, with `R` the regular +representation, is `D` copies of `R` and contains every irreducible representation of `G`. By Burnside's theorem +every irreducible representation of `G` occurs in some tensor power `rho^{(x) m}`, `m >= 0`, so every irreducible +representation occurs in some `rho^{(x) (m+1)}` with `m + 1 >= 1`. Hence `a` acts as zero in every irreducible +representation, and `a = 0` in `C[G]`. ∎ + +Three consequences are used below. + +1. **Group identities lift.** If two products of native generators are the same element of `G` (same Pauli + tableau and same action on the basis state `|0>`, which fixes the absolute phase), they agree at every width. + This covers inverses, exponent two (`C_0^2 = X_0`), commutation of operators on disjoint axes, Hadamard + children, phases and spectators (tensoring with the identity on the untouched axes is again an element of the + larger Clifford group). +2. **Free-word identities lift.** An identity that holds in the free group algebra on the native symbols, with + only adjacent inverse cancellation, holds in `C[G]` under every assignment of symbols to group elements, hence at + every width. +3. **Linear relations between distinct elements do not lift.** `C_0 = (1+i)/2 I + (1-i)/2 X_0` is an identity of + matrices at width one and a nonzero element of `C[G]` (three distinct group elements); it fails at width two. + The same holds for the scalar `i` against the element `iI`, whose tensor square is `-I`. A certificate must + therefore keep the scalar layer and the group layer apart, exactly as the selected convention prescribes. + +The census `a = 0 in C[G]` is a complete decision procedure: no finite set of widths has to be evaluated. PR5369 and +PR5376 prove the same criterion in the quantitative form of finite width cutoffs (four and eight widths), which is +what one needs when the distinct group elements cannot be canonicalized; here they can, by `clifford_exact.py`. + +## 3. The selected caller as a composition of liftable identities + +The runtime of PR5413 is the controller `NEUTRAL-CALLER-v16c` with eighteen backward calls of the body +`NEUTRAL-BACKWARD-v16c`, whose `PROVIDER_5402` is the changed #5383 word with the port wrappers of +`NORMALIZERS.json`. [verify.py](verify.py) checks the following. + +**A. Port binding (896 exact group identities).** For each of the 112 ports and both orientations, the physical +path operators of the body are, with absolute phase, + + x -> X : D, y -> Y : D, y -> X : D C_0, Q_p := A_y A_x^-1 = C_0, + +where `A_role` is the input wrapper followed by the inverse canonical chart of the entrance frame, `O_role` the +canonical chart of the exit frame followed by the output wrapper, `D` the positive rank-eight Gaussian on axes 1..8 +and `C_0` the positive central Gaussian on axis 0. The backward orientation uses the entrywise-conjugate chart and +operator semantics of PR5376 `PROVIDER.md`; mixing conventions produces a different element on every port. These +are statements about elements of `G`, so by consequence 1 they hold at every width: the body is the controller's +`X = D x - D Q y`, `Y = D y` on every column. + +**B. Body endpoint (free-word identity).** The free-word replay of the body with the provider expanded ends with +every native warp cancelled, the main rows `X_p = Nout_x (Nin_x x_p - Nin_y y_p)` and `Y_p = Nout_y Nin_y y_p` +carrying only the port wrappers, the 400 autonomous helpers returned as their own input under an alias pair of exact +signed monomials (318 pure central phases, 82 with an address action; none is the identity) with the recorded exit +frame reached by their paid climbs, the eight mode owners returned as the paid rank-eight Gaussian of `h - Z y` (own input plus 56 `y` +inputs with `±1/2` entries), and all seventeen owned fields zero. By consequence 2 this endpoint is the same at +every width. Combined with A, the body's physical endpoint on main data is exactly `D x - D C_0 y`, `D y`. + +**C. Controller (free commutative identity, abelian realization).** The controller's thirty-two bank rows are +replayed in the free commutative Laurent ring on `Q` and `D_1, ..., D_33` (the semantics of +`check_wholecaller_v1.py`, no finite-order quotient); the endpoint is the recorded diagonal with exterior +coefficient `+1`. The plan `WHOLECALLER-PLAN-v1.json` realizes `Q = C_0` on the global central axis 0 and `D_s` as +the rank-eight Gaussian on the eight private axes of stage `s`; the eighteen private planes are pairwise disjoint +and disjoint from axis 0, so all realized symbols commute as exact group elements. A polynomial identity in +commuting invertible variables holds for any commuting invertible assignment, in particular for the tensor powers +`C_0^{(x) f}` and `D_s^{(x) f}`, which still commute. The sixteen banks whose diagonal carries `Q^{-1}` are +corrected by the central translation `X_0 = C_0^2`, and `C_0^{-1} X_0 = C_0` is an exact group identity (phase +included), so every main target is the positive canonical Gaussian with absolute phase at every width. The scalar +`Q_POWER` events are `X_0^{±1}` (even exponents), and the signed swaps use the fixed scalar `-1`. + +**Conclusion.** The complete caller identity of PR5413 is a composition of identities of types 1 and 2, with +fixed real dyadic coefficients. Each lifts to every positive column multiplicity. This is the algebraic half of +the retained assumption `native_all_columns` for the selected caller. It does not address the physical half: that +the lifted operators, spectators and whole-job adapters are realized on the fixed tape at the retained tariff. + +## 4. Controls + +[verify.py](verify.py) evaluates the four traps of section 2 on dense `2x2` and `4x4` matrices over `Q(i)`: the +Reynolds-type relation and the scalar phase trap vanish at width one and fail at width two, while the census +reports three and two distinct elements; exponent two is one element written two ways and vanishes at widths one to +three; reversed noncommuting factors are distinct elements and already differ at width one. [test_verify.py](test_verify.py) +rejects: input drift, a wrapper phase mutation, a mixed-convention reading, a leftover native warp in the body +endpoint, an owned field left nonzero, overlapping private planes, a missing `Q_POWER`, and a tampered result. diff --git a/research/allwidth-caller-certificate/README.md b/research/allwidth-caller-certificate/README.md new file mode 100644 index 0000000000..15946214c7 --- /dev/null +++ b/research/allwidth-caller-certificate/README.md @@ -0,0 +1,61 @@ +# All-width certificate for the complete selected #5413 caller + +**Scoped positive result; no new κ.** The complete caller identity of +[PR #5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413) holds at every positive column multiplicity, +and the proof is a census of exact group elements that a small checker verifies. This is target 8 of +[PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428): compact all-width native identity +certificates. It discharges the algebraic half of the retained assumption `native_all_columns` for the selected +caller; the physical half (tape realization of the lifted operators with spectators and adapters at the retained +tariff) is left explicit and untouched. + +## Lemma + +For a finite group `G` of exact matrices and fixed coefficients `c_g`, + + sum_g c_g g^{(x) f} = 0 for every f >= 1 <=> sum_g c_g g = 0 in C[G]. + +The map `g -> g^{(x) f}` is a group homomorphism, so group identities and free-word identities lift; by Burnside a +nonzero element of `C[G]` fails at some width. [PROOF.md](PROOF.md) gives the proof and the three consequences +used. The census replaces the finite width cutoffs of [PR5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369) +and [PR5376](https://github.com/CrocSwap/integer-mult-bounds/pull/5376) whenever the elements can be canonicalized, +which `clifford_exact.py` does (Pauli tableau plus the image of `|0>`, fixing the absolute phase). + +## What [verify.py](verify.py) certifies + +| Layer | Identity | Count | Lifts because | +|---|---|---|---| +| Ports | `x->X = D`, `y->Y = D`, `y->X = D C_0`, `Q_p = C_0`, both orientations, absolute phase | 896 | group identities | +| Body | free-word endpoint of `NEUTRAL-BACKWARD-v16c` with `PROVIDER_5402` expanded: all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under exact signed alias monomials (318 pure phases, 82 with address action) in their recorded exit frames, 8 mode outputs `C8 (h - Z y)`, 17 owned fields zero | 649 rows | free-word identity | +| Controller | Laurent replay in free commuting `Q, D_1..D_33` reproduces the diagonal; 18 private planes disjoint and disjoint from axis 0; `C_0^2 = X_0`, `C_0^-1 X_0 = C_0`, `[C_0, D] = 0` exact | 32 banks | commutative identity, abelian realization | + +Backward uses the entrywise-conjugate semantics of PR5376 `PROVIDER.md`. Reading the backward wrappers against +unconjugated charts gives a different element on every port (port 0: `-C_0^-1 Z_1 Z_2`), so the convention is part +of the certificate. + +Controls on dense `Q(i)` matrices: the Reynolds-type relation `C_0 = (1+i)/2 I + (1-i)/2 X_0` and the scalar trap +`i = iI` vanish at width 1 and fail at width 2 while the census counts three and two distinct elements; exponent two +(`C_0^2 = X_0`) is one element and lifts; reversed noncommuting factors differ already at width 1. +[test_verify.py](test_verify.py) rejects eight mutations. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/allwidth-caller-certificate +``` + +`verify.py` runs in about 40 seconds with the standard library. `RESULT.json` is rebuilt and compared. + +## Open next questions + +- The physical half of `native_all_columns` for this caller: can the distinct exact group elements used (wrappers, + `D`, `C_0`, `X_0`, the plan's `J` routes) be reduced to a finite list of fixed-tape primitives whose cost at width + `f` is the retained tariff? This is target 10 of PR #5428, not a symbolic certificate. +- The same census for the forward body (`NEUTRAL-FORWARD-v16c`, review only; it does not run in the selected + controller). + +## Not claimed + +No new κ, no selected-record change, no physical tape implementation, no independent human or kernel review. +Credit: PR5413 (Clear1nsight), PR5402 (dillona), PR5383/PR5398 (aliromman), PR5369/PR5376 (aliromman) for the +width-cutoff theorems and the orientation semantics, the Clifford compiler lineage, and PR5428 (zxv) for the target. +Prepared with substantial Claude Code assistance. diff --git a/research/allwidth-caller-certificate/RESULT.json b/research/allwidth-caller-certificate/RESULT.json new file mode 100644 index 0000000000..2671daaf46 --- /dev/null +++ b/research/allwidth-caller-certificate/RESULT.json @@ -0,0 +1,65 @@ +{ + "body_endpoint": { + "autonomous_helpers": 400, + "block_monomials_identity": 448, + "distinct_warp_symbols": 72, + "exit_frames_recorded": 632, + "helper_alias_pairs_pure_phase": 318, + "helper_alias_pairs_with_address_action": 82, + "main_rows": "X_p = Nout_x(Nin_x x_p - Nin_y y_p), Y_p = Nout_y Nin_y y_p on all 112 ports", + "mode_outputs": 8, + "mode_terms": 456, + "owned_zero": 17, + "warps_cancelled": true + }, + "conclusion": "The complete #5413 caller identity is a composition of (i) a free-word identity of the body, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.", + "controller": { + "central_axis": 0, + "group_identities": [ + "C_0^2 = X_0", + "C_0^-1 X_0 = C_0", + "[C_0, D] = 0" + ], + "laurent_endpoint": "diagonal, exterior coefficient +1, no finite-order quotient", + "negative_q_banks": 16, + "private_axes_disjoint": true, + "q_power_exponents": [ + -2, + 2 + ], + "stages": 18 + }, + "lemma": "sum_g c_g g^{(x)f} = 0 for all f >= 1 <=> sum_g c_g g = 0 in C[G]; group identities lift by g -> g^{(x)f}", + "lemma_controls": { + "exponent_two": { + "same_element": true, + "widths_zero": [ + true, + true, + true + ] + }, + "reversed_factors": { + "same_element": false, + "width1_zero": false + }, + "reynolds_trap": { + "distinct_elements": 3, + "width1_zero": true, + "width2_zero": false + }, + "scalar_phase_trap": { + "distinct_elements": 2, + "width1_zero": true, + "width2_zero": false + } + }, + "port_bindings": { + "backward_semantics": "entrywise conjugate charts and operators (PR5376 PROVIDER.md); the mixed reading differs from C_0 on all 112 ports", + "group_identities": 896, + "symbols": { + "D": "fourier on axes 1..8 (positive rank-eight Gaussian)", + "Q": "C_0 (positive central Gaussian, axis 0)" + } + } +} diff --git a/research/allwidth-caller-certificate/SOURCES.json b/research/allwidth-caller-certificate/SOURCES.json new file mode 100644 index 0000000000..804edf50af --- /dev/null +++ b/research/allwidth-caller-certificate/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "usage": "input", + "git_blob": "04c6c7f36cb1b9fcf0b464bad3d3d83aaae7c864", + "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json", + "usage": "input", + "git_blob": "975714d0c15714070b2303ca48d31871f2095210", + "sha256": "1f17fda221bc781ca0b2a120916ed500ba84c305a916a65436a5d6c72d116bcf" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", + "usage": "input", + "git_blob": "b868fe46ce7ff96a51f7b612758685a23014d31d", + "sha256": "a02e79fb4615f4f987e3b3617c2b42eea2c1d7415cc66fa702a8b0cd28e6387e" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", + "usage": "input", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz", + "usage": "input", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + }, + { + "path": "research/eight-owned-relations/WORD.json.gz", + "usage": "input", + "git_blob": "c62fcb59643f87919208100517a2fbc4b57cb7d7", + "sha256": "6412632c28e265597fb088087048091d81c19500fb28a0c9c9d2a48f61b8665b" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/allwidth-caller-certificate/TASK.json b/research/allwidth-caller-certificate/TASK.json new file mode 100644 index 0000000000..d3bb4fe686 --- /dev/null +++ b/research/allwidth-caller-certificate/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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": "Does the complete selected #5413 caller identity hold at every positive column multiplicity, as a checkable certificate in the group algebra of its exact native operators (ports, body, controller)?", + "scope_change_reason": "Target 8 of PR #5428 asks for compact all-width native identity certificates. PR5369/PR5376 settle the selected local provider; the selected result now runs that word inside the #5413 body and 145-axis controller, whose all-width phase argument is prose in WHOLECALLER-PLAN-v1. This package states the lifting lemma and binds it to the actual caller with an executable census.", + "bottleneck_link": "Side result; no new kappa. It discharges the algebraic half of native_all_columns for the selected caller and leaves the physical half (tape realization at width f) explicit.", + "budget_minutes": 240, + "stop_rule": "Stop at the composite certificate of the selected caller; the physical implementation of lifted operators is a separate (direction 10) question.", + "outcome": "completed", + "evidence": "verify.py: 896 exact group identities bind every port path to the controller symbols D and C_0 with absolute phase in both orientations (the mixed orientation convention differs on all 112 ports); the free-word body replay with the #5402 provider expanded ends with every warp cancelled and only the port wrappers on main rows; the controller Laurent replay is a free commutative identity realized on 18 disjoint private planes plus the central axis, with C_0^2 = X_0 and C_0^-1 X_0 = C_0 exact; lemma controls on dense Q(i) matrices show the Reynolds and scalar-phase traps pass width 1 and fail width 2. test_verify.py rejects eight mutations.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Can the physical half of native_all_columns for this caller be reduced to a finite list of tape primitives at width f (spectator-preserving row additions, central translations, canonical rank-r children)?", + "why_it_matters": "The algebraic half is now a certificate; the retained assumption survives only as the tape realization of g^{(x)f} with spectators and whole-job adapters at the retained tariff.", + "first_step": "Enumerate the distinct exact group elements used by the caller (wrappers, D, C_0, X_0, J routes) and map each to the compact-control primitives of notes/compact-control-movement.tex with its f-dependence.", + "blocked_by": "A uniform fixed-tape implementation theorem (target 10 of PR #5428)." + } + ] +} diff --git a/research/allwidth-caller-certificate/VERIFY.json b/research/allwidth-caller-certificate/VERIFY.json new file mode 100644 index 0000000000..11972a44c1 --- /dev/null +++ b/research/allwidth-caller-certificate/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-CALLER-v16c.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz", + "research/eight-owned-relations/WORD.json.gz", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Pinned inputs; controller and plan bind the body; 896 exact group identities (112 ports, both orientations, paths x->X = D, y->Y = D, y->X = D C_0, Q_p = C_0 with absolute phase; mixed convention differs on all ports); free-word body endpoint with the #5402 provider expanded (all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under signed alias monomials in their recorded exit frames, 8 mode outputs C8 (h - Z y), 17 owned fields zero); Laurent replay reproduces the diagonal; 18 private planes disjoint from each other and from the central axis; C_0^2 = X_0, C_0^-1 X_0 = C_0, [C_0, D] = 0 exactly; even Q_POWER; 16 negative banks corrected by X; lemma controls on dense Q(i) matrices (Reynolds and scalar-phase traps pass width 1 and fail width 2, exponent two lifts, reversed factors differ); stored RESULT.json equals the rebuild." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 600, + "checks": "Rejecting controls: input drift, a wrapper phase mutation, the mixed orientation convention, a leftover native warp at the body endpoint, an owned field not cleared, overlapping private planes, a missing controller Q_POWER, tampered RESULT.json." + } + ] +} diff --git a/research/allwidth-caller-certificate/test_verify.py b/research/allwidth-caller-certificate/test_verify.py new file mode 100644 index 0000000000..629cd542a7 --- /dev/null +++ b/research/allwidth-caller-certificate/test_verify.py @@ -0,0 +1,99 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit('FAIL...').""" +import copy +import gzip +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +CE = V.load_clifford() +BODY = json.loads(V.BODY.read_text(encoding='utf-8')) +CALLER = json.loads(V.CALLER.read_text(encoding='utf-8')) +PLAN = json.loads(V.PLAN.read_text(encoding='utf-8')) +PROV = json.loads((V.PROV / 'PROVIDER.json').read_text(encoding='utf-8')) +WORD = json.loads(gzip.decompress((V.PROV / 'WORD.json.gz').read_bytes())) +CAN = json.loads(gzip.decompress(V.EIGHT.read_bytes()))['canonical'] +NORM = json.loads(V.NORM.read_text(encoding='utf-8')) + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith('FAIL'): + raise + print('rejected:', name) + return + raise AssertionError('control accepted: ' + name) + + +def drift(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + row = next(r for r in rows['files'] if r['usage'] == 'input') + data = (V.ROOT / row['path']).read_bytes() + V.require(V.hashlib.sha256(data).hexdigest() == '0' * 64, 'input drift: ' + row['path']) + + +def wrapper_phase(): + nz = copy.deepcopy(NORM) + word = nz['ports'][7]['compiled_wrappers']['backward_input_X']['word'] + ph = next(e for e in word if e[0] == 'phase'); ph[1] = (ph[1] + 1) % 4 + V.port_bindings(V.Ops(CE, CAN, nz)) + + +def mixed_convention(): + ops = V.Ops(CE, CAN, NORM) + ops.conj = lambda op: op # read the backward wrappers against unconjugated charts + V.port_bindings(ops) + + +def leftover_warp(): + word = copy.deepcopy(WORD) + ev = next(e for e in word['word'] if e[0] == 'warp' and e[1][0] == 'L' and e[1][1] < 112) + word['word'].remove(ev) # its inverse partner no longer cancels + B = V.Body(BODY, PROV, word, CAN); B.run() + V.body_endpoint(B, V.Ops(CE, CAN, NORM)) + + +def owned_not_cleared(): + body = copy.deepcopy(BODY) + body['operations'] = [o for o in body['operations'] if o['op'] != 'CLEAR'] + B = V.Body(body, PROV, WORD, CAN); B.run() + + +def overlapping_planes(): + plan = copy.deepcopy(PLAN) + plan['stage_embeddings'][1]['local_axes'] = plan['stage_embeddings'][0]['local_axes'] + V.controller_realization(V.Ops(CE, CAN, NORM), CALLER, plan) + + +def missing_q_power(): + caller = copy.deepcopy(CALLER) + ev = caller['controller']['physical_events'] + ev.pop(next(i for i, e in enumerate(ev) if e[0] == 'Q_POWER')) + V.laurent(caller['controller']) + + +def tampered_result(): + stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + bad = copy.deepcopy(stored); bad['port_bindings']['group_identities'] = 895 + V.require(bad == stored, 'stored RESULT.json equals the rebuild') + + +def main(): + rejects('input drift', drift) + rejects('wrapper phase mutation (port 7)', wrapper_phase) + rejects('mixed orientation convention', mixed_convention) + rejects('leftover native warp at the endpoint', leftover_warp) + rejects('owned field not cleared', owned_not_cleared) + rejects('overlapping private planes', overlapping_planes) + rejects('missing controller Q_POWER', missing_q_power) + rejects('tampered RESULT.json', tampered_result) + print('PASS_ALLWIDTH_CALLER_CERTIFICATE_CONTROLS') + + +if __name__ == '__main__': + main() diff --git a/research/allwidth-caller-certificate/verify.py b/research/allwidth-caller-certificate/verify.py new file mode 100644 index 0000000000..d63d4aca47 --- /dev/null +++ b/research/allwidth-caller-certificate/verify.py @@ -0,0 +1,580 @@ +"""All-width certificate for the complete selected #5413 caller, in the group algebra of its native operators. + +Lifting lemma (PROOF.md). Let G be a finite group of exact matrices (here: the dyadic Clifford group on nine or +145 binary axes, absolute phase included) and let a = sum_g c_g g be an element of C[G] with fixed coefficients. +Then sum_g c_g g^{(x) f} = 0 for every positive column multiplicity f <=> a = 0 in C[G]. +The map g -> g^{(x) f} is a group homomorphism, so any identity between products of group elements, and any +identity of C[G], transfers to every width. Conversely an element that is not zero in C[G] fails at some width +(Burnside). A certificate is therefore a census of exact group elements: canonical tableau plus the action on the +basis state |0>, which fixes the absolute phase. Scalar coefficients stay outside the tensor power; the central +scalars i^k I are group elements, not coefficients. + +What this file certifies for the selected caller (PR #5413, selected at the pinned base): + A. Port binding (896 group identities, both orientations, exact phase). For every port p the physical paths of + the body are x->X = D, y->Y = D, y->X = D C_0 and the query operator Q_p = A_y A_x^-1 = C_0, where D is the + positive rank-eight Gaussian on axes 1..8 and C_0 the positive central Gaussian on axis 0. The backward + orientation uses the entrywise-conjugate frame semantics; without the conjugation the element is -conj(C_0). + B. Body endpoint (free-word replay of NEUTRAL-BACKWARD-v16c with the #5402 provider expanded): every surviving + term of the main endpoint carries only the port wrappers; every warp cancelled; the 400 autonomous helper + rows are wrapper pairs; owned fields zero. Free-word identities are identities of C[G] for every assignment. + C. Controller: the exact Laurent replay of check_wholecaller_v1 in free commuting variables Q, D_s; the plan's + 18 stage planes are pairwise disjoint and disjoint from the central axis, so the realization Q = C_0, + D_s = fourier(stage axes) is abelian; C_0^2 = X_0 and C_0^-1 X_0 = C_0 exactly, so the 16 negative diagonal + exponents are corrected by the central translation inside the group. + D. Controls of the lemma on small matrices: the Reynolds-type trap C_0 = (1+i)/2 I + (1-i)/2 X_0 and the scalar + trap i*I = (iI) hold at width 1 and fail at width 2 while the census rejects them; exponent two and reversed + factors behave as the census predicts. +No new kappa. The physical half of native_all_columns (tape realization of g^{(x) f} with spectators and adapters +at the retained tariff) is not addressed here. +""" +import argparse +import collections +import gzip +import hashlib +import importlib.util +import json +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +CAP = ROOT / 'research' / 'coupled-helper-neutral-completion' / 'capsule' / 'workspace' +BODY = CAP / 'swarm-coupled-caller-sol-high-20261024' / 'agents' / 'caller' / 'NEUTRAL-BACKWARD-v16c.json' +CALLER = CAP / 'swarm-coupled-caller-sol-high-20261024' / 'agents' / 'caller' / 'NEUTRAL-CALLER-v16c.json' +PLAN = CAP / 'swarm-coupled-caller-sol-high-20261024' / 'agents' / 'challenge' / 'WHOLECALLER-PLAN-v1.json' +PROV = CAP / 'swarm-provider-audit-sol-high-20261024' / 'repository' / 'research' / 'native-rank8-helper-provider' +NORM = CAP / 'swarm-provider-audit-sol-high-20261024' / 'agents' / 'budget' / 'inputs' / 'NORMALIZERS.json' +EIGHT = ROOT / 'research' / 'eight-owned-relations' / 'WORD.json.gz' +CLIFFORD = ROOT / 'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py' +N9 = 9 + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +def load_clifford(): + spec = importlib.util.spec_from_file_location('allwidth_clifford_exact', CLIFFORD) + ce = importlib.util.module_from_spec(spec); spec.loader.exec_module(ce) + return ce + + +def elem(op): + """Exact group element: Pauli tableau (Clifford up to phase) and the image of |0> (fixes the phase).""" + vec, den = op.zero_state() + return op.tab, tuple(vec), den + + +class Ops: + """Nine-axis Clifford helpers: charts (plain or entrywise conjugate), monomial words, native warps.""" + + def __init__(self, ce, canonical, normalizers): + self.ce, self.c, self.nz = ce, canonical, normalizers + self.charts, self.kc = {}, {} + self.warp = {w['op']: w['G_columns'] for w in canonical['warps']} + self.I = ce.ident(N9) + self.C0 = ce.cgate(N9, 1, 1) + self.C0inv = ce.cgate(N9, 1, -1) + self.X0 = ce.xgate(N9, 1) + self.D = ce.fourier(N9, range(1, 9)) + + def phase(self, k): + return self.ce.Op(N9, self.ce.identity(N9), [('phase', k % 4)]) + + def mono(self, word): + ce = self.ce; op = ce.ident(N9) + for e in word: + if e[0] == 'D': + op = op.then(ce.diag(N9, e[1], e[2])) + elif e[0] == 'P': + op = op.then(ce.perm(N9, e[1])) + elif e[0] == 'X': + op = op.then(ce.xgate(N9, e[1])) + elif e[0] == 'phase': + op = op.then(self.phase(e[1])) + else: + require(False, 'unknown monomial primitive') + return op + + def conj(self, op): + """Entrywise complex conjugate of an exact circuit (the backward native semantics).""" + ce = self.ce; r = ce.ident(N9) + for g in op.circuit: + if g[0] == 'P': + part = ce.perm(N9, g[1]) + elif g[0] == 'X': + part = ce.xgate(N9, g[1]) + elif g[0] == 'C': + part = ce.cgate(N9, g[1], -g[2]) + elif g[0] == 'D': + part = ce.diag(N9, g[1], tuple(-x % 4 for x in g[2])) + else: + part = self.phase(-g[1]) + r = r.then(part) + return r + + def chart(self, f, cj=False): + if (f, cj) not in self.charts: + op = self.ce.canonical_frame(N9, self.c['frames'][f]) + self.charts[(f, cj)] = self.conj(op) if cj else op + return self.charts[(f, cj)] + + def K(self, sym): + if sym not in self.kc: + ce = self.ce + G = ce.transpose(tuple(self.warp[abs(sym)]), N9); gi = ce.inv(G, N9); tr = ce.transpose(gi, N9) + quad = tuple((1 << i) ^ sum(ce.parity(a & b) << j for j, b in enumerate(tr)) for i, a in enumerate(tr)) + k = ce.perm(N9, G).then(ce.diag(N9, quad)) + self.kc[sym] = k if sym > 0 else k.adjoint() + return self.kc[sym] + + def paths(self, p, backward): + """Physical path operators of port p through the body, with the port wrappers of NORMALIZERS.json. + + A_role = input wrapper, then inverse canonical chart of the role's entrance frame; + O_role = canonical chart of the role's exit frame, then output wrapper. The body's logical endpoint is + X = x - y, Y = y, so x->X = A_x O_x, y->Y = A_y O_y, y->X = A_y O_x and the query operator is Q = A_y A_x^-1. + """ + wr = self.nz['ports'][p]['compiled_wrappers']; pre = 'backward_' if backward else ''; cj = backward + Ax = self.mono(wr[pre + 'input_X']['word']).then(self.chart(self.c['start'][p], cj).adjoint()) + Ay = self.mono(wr[pre + 'input_Y']['word']).then(self.chart(self.c['start'][p + 112], cj).adjoint()) + Ox = self.chart(self.c['final'][p], cj).then(self.mono(wr[pre + 'output_X']['word'])) + Oy = self.chart(self.c['final'][p + 112], cj).then(self.mono(wr[pre + 'output_Y']['word'])) + return {'Q': Ay.then(Ax.adjoint()), 'x->X': Ax.then(Ox), 'y->Y': Ay.then(Oy), 'y->X': Ay.then(Ox)} + + +def port_bindings(ops): + """A: 112 ports x 2 orientations x 4 paths are the controller's abelian symbols, with exact absolute phase.""" + want = {'Q': elem(ops.C0), 'x->X': elem(ops.D), 'y->Y': elem(ops.D), 'y->X': elem(ops.D.then(ops.C0))} + count = 0 + for backward in (False, True): + for p in range(112): + got = ops.paths(p, backward) + for name, op in got.items(): + require(elem(op) == want[name], 'port %d %s path %s is not the controller symbol' % (p, 'backward' if backward else 'forward', name)) + count += 1 + # The orientation convention matters: reading the backward wrappers against plain (unconjugated) charts gives a + # different group element on every port (on port 0: -C_0^-1 times Z_1 Z_2, phase -1), so a census that mixed the + # two conventions would wrongly reject the binding. Only the conjugate reading is the backward semantics. + mixed = 0 + for p in range(112): + wr = ops.nz['ports'][p]['compiled_wrappers'] + Ax = ops.mono(wr['backward_input_X']['word']).then(ops.chart(ops.c['start'][p]).adjoint()) + Ay = ops.mono(wr['backward_input_Y']['word']).then(ops.chart(ops.c['start'][p + 112]).adjoint()) + mixed += elem(Ay.then(Ax.adjoint())) != want['Q'] + require(mixed == 112, 'the mixed-convention reading is a different element on every port') + return dict(group_identities=count, symbols=dict(Q='C_0 (positive central Gaussian, axis 0)', + D='fourier on axes 1..8 (positive rank-eight Gaussian)'), + backward_semantics='entrywise conjugate charts and operators (PR5376 PROVIDER.md); the mixed reading differs from C_0 on all 112 ports') + + +class Body: + """Free-word replay of the runtime body (NEUTRAL-BACKWARD-v16c with PROVIDER_5402 expanded by its schedule). + + Rows are keyed by (input field, word of symbols). Native warps are the symbols ('W', op) with adjacent + inverse cancellation; wrappers, monomials and Gaussians are fresh symbols, so no term through a different + operator path ever merges. A free-word endpoint is an identity of C[G] under every assignment of group + elements to symbols, hence an identity at every column width. + """ + + def __init__(self, body, prov, word, canonical): + self.ops_list = body['operations'] + self.body, self.prov, self.word, self.c = body, prov, word, canonical + self.bind = body['physical_field_bindings'] + self.rows = {i: {(i, ()): F(1)} for i in range(body['physical_field_count'])} + self.sym = 0; self.meaning = {} + + def newsym(self, tag, meaning=None): + self.sym += 1 + self.meaning[(tag, self.sym)] = meaning + return (tag, self.sym) + + def apply(self, f, s): + out = {} + for (inp, wd), q in self.rows[f].items(): + nw = wd[:-1] if s[0] == 'W' and wd and wd[-1] == ('W', -s[1]) else wd + (s,) + v = out.get((inp, nw), 0) + q + if v: + out[(inp, nw)] = v + else: + out.pop((inp, nw), None) + self.rows[f] = out + + def add(self, dst, src, q): + d = self.rows[dst] + for k, v in self.rows[src].items(): + nv = d.get(k, 0) + q * v + if nv: + d[k] = nv + else: + d.pop(k, None) + + def scale(self, f, q): + self.rows[f] = {k: q * v for k, v in self.rows[f].items()} + + @staticmethod + def role(r): + if isinstance(r, int): + return r + return r[1] if r[0] == 'L' else 632 + r[1] + + def provider(self): + p = self.prov + for f in range(224): + self.apply(f, self.newsym('Nin', f)) + for m in p['mode_boundaries']: + self.apply(m['owner'], self.newsym('K', m['owner'])); self.scale(m['owner'], F(2)) + for ins in p['input_basis_program']: + if ins[0] == 'add': + self.add(ins[1], ins[2], F(ins[3])) + else: + self.scale(ins[1], F(ins[2])) + self.frames = {i: self.c['start'][i] for i in range(632)} + for e in self.word['word']: + k = e[0] + if k == 'warp': + self.apply(self.role(e[1]), ('W', e[2])) + if e[1][0] == 'L': + self.frames[e[1][1]] = e[4] + elif k == 'climb': + self.frames[e[2]] = e[4] + elif k == 'scalar': + g = e[1]; d_ = self.role(g[1]) + if g[1][0] == 'L' and e[2] is not None: + self.frames[g[1][1]] = e[2] + if g[0] == 'clear': + self.rows[d_] = {} + elif g[0] == 'copy': + self.rows[d_] = dict(self.rows[self.role(g[2])]) + elif g[0] == 'add': + self.add(d_, self.role(g[2]), F(g[3], g[4])) + elif g[0] == 'scale': + self.scale(d_, F(g[2], g[3])) + else: + require(False, 'unknown provider scalar') + elif k == 'zero_retag': + require(not self.rows[self.role(e[1])], 'provider zero retag on a zero row') + else: + require(k in ('climb', 'center', 'adapter', 'phase'), 'unknown provider event') + for ins in p['output_basis_program']: + if ins[0] == 'add': + self.add(ins[1], ins[2], F(ins[3])) + else: + self.scale(ins[1], F(ins[2])) + for m in p['mode_boundaries']: + cs, o = m['cache_slot'], m['owner'] + self.scale(cs, F(m['cache_scalar'])); self.apply(cs, self.newsym('N', o)) + require(not self.rows[o], 'mode owner zero before the cache SWAP') + self.rows[cs], self.rows[o] = self.rows[o], {} + for f in range(224): + self.apply(f, self.newsym('Nout', f)) + + def run(self): + b = self.bind + for o in self.ops_list: + k = o['op'] + if k == 'MONOMIAL': + self.apply(b[o['field']], self.newsym('M', o['word'])) + elif k == 'GAUSSIAN': + self.apply(b[o['field']], self.newsym('G', o['operator'])) + elif k == 'ADD': + self.add(b[o['dst']], b[o['src']], F(o['coefficient'])) + elif k == 'CLEAR': + self.rows[b[o['field']]] = {} + elif k == 'ZERO_RETAG': + require(not self.rows[b[o['field']]], 'body zero retag on a zero row') + elif k == 'SWAP': + x, y = (b[f] for f in o['fields']); self.rows[x], self.rows[y] = self.rows[y], self.rows[x] + elif k == 'PROVIDER_5402': + self.provider() + else: + require(False, 'unknown body operation ' + k) + owned = [b[f] for f in b if f[0] in 'ct'] + require(len(owned) == 17 and all(not self.rows[f] for f in owned), 'all 17 owned fields zero at exit') + + +def body_endpoint(B, ops): + """B: the main endpoint carries only the port wrappers, every warp cancelled; helpers are autonomous.""" + warps_left = sum(1 for f in range(649) for (inp, wd) in B.rows[f] for s in wd if s[0] == 'W') + require(warps_left == 0, 'every native warp cancels in the free group at the endpoint') + block_maps = 0 + + def strip_block(wd): + """The body's y-field block is a monomial, ADDs, and the exact inverse monomial: an identity element.""" + nonlocal block_maps + ms = [s for s in wd if s[0] == 'M'] + if ms: + m = ops.I + for s in ms: + m = m.then(ops.mono(B.meaning[s])) + require(elem(m) == elem(ops.I), 'block monomials on a main row compose to the identity element') + block_maps += len(ms) + return tuple(s for s in wd if s[0] != 'M') + for p in range(112): + X = B.rows[p]; Y = B.rows[p + 112] + require(len(X) == 2 and len(Y) == 1, 'main rows X: two terms, Y: one term') + for (inp, wd), q in X.items(): + wd = strip_block(wd); tags = tuple(s[0] for s in wd) + require(tags == ('Nin', 'Nout') and B.meaning[wd[1]] == p, 'X term is wrapped by the port wrappers only') + if inp == p: + require(q == 1 and B.meaning[wd[0]] == p, 'x_p term: coefficient 1, x input wrapper') + else: + require(inp == p + 112 and q == -1 and B.meaning[wd[0]] == p + 112, 'y_p term: coefficient -1, y input wrapper') + (inp, wd), q = next(iter(Y.items())); wd = strip_block(wd) + require(inp == p + 112 and q == 1 and tuple(s[0] for s in wd) == ('Nin', 'Nout') + and B.meaning[wd[0]] == p + 112 and B.meaning[wd[1]] == p + 112, 'Y row is the wrapped y_p') + # the 400 autonomous helpers return as their own input under an alias pair of monomials (an exact group + # element pair, inverse to each other); the 8 mode owners return the paid rank-8 Gaussian of h_mode - Z y with + # fixed +-1/2 entries over 56 y inputs (the restored coupled outputs, counted as paid+productive by #5413). + autonomous = 0; alias_pairs_identity = 0; modes = 0; mode_terms = 0 + mode_owners = set(B.prov['mode_owners']) + for h in range(224, 632): + r = B.rows[h] + if h in mode_owners: + modes += 1; mode_terms += len(r) + # H = D (h - Z y): own input with coefficient 1 and 56 y inputs with +-1/2 (Z = diag M^T diag / 2), one C8. + require(len(r) == 57 and sum(1 for (inp, wd) in r if inp == h) == 1, 'mode output: own input plus 56 y inputs') + for (inp, wd), q in r.items(): + require((q == 1 if inp == h else 112 <= inp < 224 and abs(q) == F(1, 2)) and [s[0] for s in wd].count('G') == 1, + 'mode output: one paid Gaussian of h_mode - Z y with +-1/2 entries') + continue + require(len(r) == 1, 'autonomous helper returns one term') + (inp, wd), q = next(iter(r.items())) + require(inp == h and q == 1 and tuple(s[0] for s in wd) == ('M', 'M'), 'helper returns itself under two monomials') + m = ops.mono(B.meaning[wd[0]]).then(ops.mono(B.meaning[wd[1]])) + require(ops.ce.rank([x for x, z, ph in m.tab[N9:]]) == 0, 'helper alias pair is a monomial (rank 0) element') + require(elem(m) != elem(ops.I), 'helper alias pairs are nontrivial (signed) monomials') + if m.tab == ops.I.tab: + alias_pairs_identity += 1 # identity tableau: a pure central phase i^k + autonomous += 1 + require(autonomous == 400 and modes == 8, '400 autonomous helpers, 8 modes') + # the paid climbs of every persistent role telescope to the recorded exit frame (frame changes are inert in rows) + require(all(B.frames[i] == B.c['final'][i] for i in range(632)), 'every persistent role ends in its recorded exit frame') + return dict(warps_cancelled=True, main_rows='X_p = Nout_x(Nin_x x_p - Nin_y y_p), Y_p = Nout_y Nin_y y_p on all 112 ports', + block_monomials_identity=block_maps, exit_frames_recorded=632, + autonomous_helpers=400, helper_alias_pairs_pure_phase=alias_pairs_identity, + helper_alias_pairs_with_address_action=400 - alias_pairs_identity, mode_outputs=8, mode_terms=mode_terms, + distinct_warp_symbols=len({abs(e[2]) for e in B.word['word'] if e[0] == 'warp'}), owned_zero=17) + + +def laurent(controller): + """check_wholecaller_v1 semantics: 32 banks, free commuting Laurent variables Q and D_1..D_33.""" + def add(a, b, c=1): + out = dict(a) + for k, v in b.items(): + out[k] = out.get(k, F(0)) + c * v + if not out[k]: + del out[k] + return out + + def mul(a, q=0, stages=()): + out = {} + for (j, e), c in a.items(): + z = list(e); z[0] += q + for s in stages: + z[s + 1] += 1 + out[j, tuple(z)] = c + return out + + def scalar(rows, prog): + r = [dict(x) for x in rows] + for op in prog: + if op[0] == 'ADD': + r[op[1]] = add(r[op[1]], r[op[2]], F(op[3])) + elif op[0] == 'SCALE': + r[op[1]] = {k: F(op[2]) * v for k, v in r[op[1]].items()} + elif op[0] == 'SWAP': + r[op[1]], r[op[2]] = r[op[2]], r[op[1]] + else: + require(False, 'boundary program primitive') + return r + w = controller + zero = (0,) * 34 + r = scalar([{(j, zero): F(1)} for j in range(32)], w['boundaries']['right_program']) + stages = set(); qpow = [] + for e in w['physical_events']: + kind = e[0] + if kind in ('LOCAL', 'QUERY_SHEAR'): + _, s, p, back = e; x, y = 2 * p, 2 * p + 1 + if back: + r[x] = add(r[x], mul(r[y], q=1), -1) + else: + r[y] = add(r[y], mul(r[x], q=-1)) + if kind == 'LOCAL': + stages.add(s); r[x] = mul(r[x], stages=[s]); r[y] = mul(r[y], stages=[s]) + elif kind == 'IDLE': + for j in (2 * e[1], 2 * e[1] + 1): + r[j] = mul(r[j], stages=e[2]) + elif kind == 'ADD': + r[e[1]] = add(r[e[1]], r[e[2]], F(e[3])) + elif kind == 'Q_POWER': + qpow.append(e[2]); r[e[1]] = mul(r[e[1]], q=e[2]) + elif kind == 'SIGNED_SWAP': + a, b = e[1:]; r[a] = add(r[a], r[b]); r[b] = add(r[b], r[a], -1); r[a] = add(r[a], r[b]) + elif kind == 'SWAP': + a, b = e[1:]; r[a], r[b] = r[b], r[a] + else: + require(False, 'unknown controller event') + r = scalar(r, w['boundaries']['left_program']) + require(r == [{(j, tuple(d)): F(1)} for j, d in enumerate(w['diagonal'])], 'Laurent endpoint is the diagonal') + return stages, qpow + + +def controller_realization(ops, caller, plan): + """C: the Laurent identity holds in free commuting variables; its realization on the plan's axes is abelian.""" + w = caller['controller'] + stages, qpow = laurent(w) + require(len(stages) == 18, 'eighteen LOCAL stages') + planes = {s['stage']: s['local_axes'] for s in plan['stage_embeddings']} + require(set(planes) == stages and plan['ambient_axes'] == 145, 'plan embeds exactly the eighteen stages on 145 axes') + private = [] + for s, axes in planes.items(): + require(axes[0] == 0 and len(axes) == 9 and all(1 <= a <= 144 for a in axes[1:]), 'stage plane: central axis 0 plus eight private axes') + private.extend(axes[1:]) + require(len(private) == 144 and len(set(private)) == 144, 'the 18 private planes are pairwise disjoint') + # exact group identities used by the plan's phase proof (nine-axis model; they are statements about C_0 and X_0 alone) + require(elem(ops.C0.then(ops.C0)) == elem(ops.X0), 'C_0^2 = X_0 with absolute coefficient +1') + require(elem(ops.C0inv.then(ops.X0)) == elem(ops.C0), 'C_0^-1 X_0 = C_0 exactly') + require(elem(ops.C0.then(ops.D)) == elem(ops.D.then(ops.C0)), 'C_0 and D commute as exact elements (disjoint axes)') + require(all(q in (-2, 2) for q in qpow), 'Q_POWER events are even central translations X_0^{+-1}') + neg = sum(1 for d in w['diagonal'] if d[0] == -1) + require(neg == 16 and all(d[0] in (-1, 1) and all(x in (0, 1) for x in d[1:]) for d in w['diagonal']), 'diagonal: Q^{+-1} times distinct D factors; 16 negative exponents') + require(all(m['central_X_after_LEFT'] == (m['q_exponent'] == -1) for m in plan['main_targets']), 'negative Q corrected by the central X in the plan') + return dict(laurent_endpoint='diagonal, exterior coefficient +1, no finite-order quotient', stages=18, + private_axes_disjoint=True, central_axis=0, q_power_exponents=sorted(set(qpow)), + negative_q_banks=neg, group_identities=['C_0^2 = X_0', 'C_0^-1 X_0 = C_0', '[C_0, D] = 0']) + + +# --- D: controls of the lifting lemma on dense matrices over Q(i), width 1 and 2 --------------------------------- +class Qi: + """Gaussian rationals a + b i with exact Fractions.""" + __slots__ = ('a', 'b') + + def __init__(self, a, b=0): + self.a, self.b = F(a), F(b) + + def __add__(self, o): + return Qi(self.a + o.a, self.b + o.b) + + def __mul__(self, o): + return Qi(self.a * o.a - self.b * o.b, self.a * o.b + self.b * o.a) + + def __eq__(self, o): + return self.a == o.a and self.b == o.b + + def __hash__(self): + return hash((self.a, self.b)) + + def __repr__(self): + return '%s%+si' % (self.a, self.b) + + +def mat(rows): + return [[x if isinstance(x, Qi) else Qi(x) for x in r] for r in rows] + + +def mmul(A, B): + n = len(A) + return [[sum((A[i][k] * B[k][j] for k in range(n)), Qi(0)) for j in range(n)] for i in range(n)] + + +def kron(A, B): + return [[A[i // len(B)][j // len(B)] * B[i % len(B)][j % len(B)] for j in range(len(A) * len(B))] for i in range(len(A) * len(B))] + + +def tpow(A, f): + out = A + for _ in range(f - 1): + out = kron(out, A) + return out + + +def msum(terms, f): + """sum_g c_g g^{(x) f} for terms (c, g) with scalar c in Q(i); the scalar stays outside the tensor power.""" + n = len(terms[0][1]) ** f + out = [[Qi(0)] * n for _ in range(n)] + for c, g in terms: + G = tpow(g, f) + out = [[out[i][j] + c * G[i][j] for j in range(n)] for i in range(n)] + return out + + +def zero(M): + return all(x == Qi(0) for r in M for x in r) + + +def lemma_controls(): + half = F(1, 2) + I = mat([[1, 0], [0, 1]]); X = mat([[0, 1], [1, 0]]); iI = mat([[Qi(0, 1), 0], [0, Qi(0, 1)]]) + C = mat([[Qi(half, half), Qi(half, -half)], [Qi(half, -half), Qi(half, half)]]) # (1+i)/2 I + (1-i)/2 X + out = {} + # (1) Reynolds-type trap: a linear relation between three distinct group elements. Width 1: zero; width 2: not. + rey = [(Qi(1), C), (Qi(-half, -half), I), (Qi(-half, half), X)] + out['reynolds_trap'] = dict(distinct_elements=3, width1_zero=zero(msum(rey, 1)), width2_zero=zero(msum(rey, 2))) + require(out['reynolds_trap']['width1_zero'] and not out['reynolds_trap']['width2_zero'], 'Reynolds trap: width 1 passes, width 2 fails') + # (2) scalar trap: the scalar i times I against the group element iI. Width 1: equal; width 2: (iI)^(x)2 = -I. + sc = [(Qi(0, 1), I), (Qi(-1), iI)] + out['scalar_phase_trap'] = dict(distinct_elements=2, width1_zero=zero(msum(sc, 1)), width2_zero=zero(msum(sc, 2))) + require(out['scalar_phase_trap']['width1_zero'] and not out['scalar_phase_trap']['width2_zero'], 'scalar phase trap: width 1 passes, width 2 fails') + # (3) exponent two: C^2 = X is one group element written two ways; it holds at every width (checked 1..3). + e2 = [(Qi(1), mmul(C, C)), (Qi(-1), X)] + out['exponent_two'] = dict(same_element=mmul(C, C) == X, widths_zero=[zero(msum(e2, f)) for f in (1, 2, 3)]) + require(out['exponent_two']['same_element'] and all(out['exponent_two']['widths_zero']), 'exponent two is a group identity') + # (4) reversed noncommuting factors: S X against X S differ as elements and already at width 1. + S = mat([[1, 0], [0, Qi(0, 1)]]) + rv = [(Qi(1), mmul(S, X)), (Qi(-1), mmul(X, S))] + out['reversed_factors'] = dict(same_element=mmul(S, X) == mmul(X, S), width1_zero=zero(msum(rv, 1))) + require(not out['reversed_factors']['same_element'] and not out['reversed_factors']['width1_zero'], 'reversed factors differ') + return out + + +def build(): + pinned_inputs() + ce = load_clifford() + body = json.loads(BODY.read_text(encoding='utf-8')) + caller = json.loads(CALLER.read_text(encoding='utf-8')) + plan = json.loads(PLAN.read_text(encoding='utf-8')) + require(caller['local_backward_sha256'] == hashlib.sha256(BODY.read_bytes()).hexdigest(), 'controller binds this body') + require(caller['runtime_local_directions'] == {'backward': 18, 'forward_macro_calls': 0}, 'only backward bodies run') + require(plan['bindings']['B_sha256'] == caller['local_backward_sha256'], 'plan binds the same body') + prov = json.loads((PROV / 'PROVIDER.json').read_text(encoding='utf-8')) + word = json.loads(gzip.decompress((PROV / 'WORD.json.gz').read_bytes())) + require(word['direction'] == 'backward', 'backward provider word') + canonical = json.loads(gzip.decompress(EIGHT.read_bytes()))['canonical'] + normalizers = json.loads(NORM.read_text(encoding='utf-8')) + require(normalizers['source_payload_sha256'] == prov['source_payload_sha256'], 'normalizers and provider share the source payload') + ops = Ops(ce, canonical, normalizers) + A = port_bindings(ops) + B = Body(body, prov, word, canonical); B.run() + Bres = body_endpoint(B, ops) + C = controller_realization(ops, caller, plan) + D = lemma_controls() + return dict(lemma='sum_g c_g g^{(x)f} = 0 for all f >= 1 <=> sum_g c_g g = 0 in C[G]; group identities lift by g -> g^{(x)f}', + port_bindings=A, body_endpoint=Bres, controller=C, lemma_controls=D, + conclusion='The complete #5413 caller identity is a composition of (i) a free-word identity of the body, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.') + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = build() + path = HERE / 'RESULT.json' + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if args.write: + path.write_bytes(text.encode('utf-8')) + require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT.json equals the rebuild') + print('PASS_ALLWIDTH_CALLER_CERTIFICATE_896_PORT_IDENTITIES_FREE_BODY_ABELIAN_CONTROLLER') + + +if __name__ == '__main__': + main() From 4d5abe038ac106bd79acf548df4aeb66f32eff09 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:07:52 +0300 Subject: [PATCH 2/2] Move the mode cache rows and certify the eight mode outputs as C8 z in C[G] The cache SWAP dropped the transformed cache row instead of moving it to the mode owner, so the package certified C8(h - Zy). With the literal SWAP each owner has 113 free-word terms; binding the provider path (input wrapper, conjugate charts, output_N) and the paid C8 path to exact group elements, the 448 cached y terms cancel the 448 y terms through C8 and each owner is exactly C8 z with absolute phase. Controls: dropped cache row, sign flip in one output_N word; the unconjugated reading leaves 896 terms. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/allwidth-caller-certificate/PROOF.md | 22 ++++- .../allwidth-caller-certificate/README.md | 5 +- .../allwidth-caller-certificate/RESULT.json | 12 ++- .../allwidth-caller-certificate/TASK.json | 2 +- .../allwidth-caller-certificate/VERIFY.json | 4 +- .../test_verify.py | 21 +++++ .../allwidth-caller-certificate/verify.py | 82 ++++++++++++++++--- 7 files changed, 123 insertions(+), 25 deletions(-) diff --git a/research/allwidth-caller-certificate/PROOF.md b/research/allwidth-caller-certificate/PROOF.md index 75ff6527c0..d9ea1027c4 100644 --- a/research/allwidth-caller-certificate/PROOF.md +++ b/research/allwidth-caller-certificate/PROOF.md @@ -70,9 +70,23 @@ are statements about elements of `G`, so by consequence 1 they hold at every wid every native warp cancelled, the main rows `X_p = Nout_x (Nin_x x_p - Nin_y y_p)` and `Y_p = Nout_y Nin_y y_p` carrying only the port wrappers, the 400 autonomous helpers returned as their own input under an alias pair of exact signed monomials (318 pure central phases, 82 with an address action; none is the identity) with the recorded exit -frame reached by their paid climbs, the eight mode owners returned as the paid rank-eight Gaussian of `h - Z y` (own input plus 56 `y` -inputs with `±1/2` entries), and all seventeen owned fields zero. By consequence 2 this endpoint is the same at -every width. Combined with A, the body's physical endpoint on main data is exactly `D x - D C_0 y`, `D y`. +frame reached by their paid climbs, and all seventeen owned fields zero. By consequence 2 this endpoint is the same +at every width. Combined with A, the body's physical endpoint on main data is exactly `D x - D C_0 y`, `D y`. + +The eight mode owners need one more step, because two different operator paths reach them. Each mode's cache SWAP +moves the provider's transformed cache row into the owner (it holds the source's `-D Z y`), and the body then adds +the owned field `T = D(S z + Z y)`, computed through one positive `C8` between alias and route monomials. As free +words the owner has 113 terms: its own input, 56 `y` terms through `C8` and 56 cached `y` terms through the +provider, which carry no `C8` symbol. The free group cannot see that they cancel, so [verify.py](verify.py) binds +every symbol to its exact element of `G`: monomials to their literal words, `G` to the positive `C8` on axes +`0..7`, `Nin_f` to the input wrapper of `f` followed by the inverse canonical chart of its entrance frame, and +`N_o` to the canonical chart of the recorded mode frame followed by the literal `output_N` word. Charts are read +in the backward (entrywise conjugate) convention, as for the ports. Summing like elements in `C[G]`, all 448 +pairs of `y` terms cancel and each owner is exactly `C8 z` with coefficient `+1` and absolute phase, which is the +source proof's `S(-DZy + D(Sz+Zy)) = S D S z = C8 z`. This is an identity in `C[G]`, so it lifts by the Lemma. +The unconjugated reading leaves all 896 `y` terms, and a sign change in one `output_N` word breaks the +cancellation; both are checked. (An earlier version of this package dropped the cache row at the SWAP and +certified `C8(h - Zy)` instead; the review of #5442 found the error.) **C. Controller (free commutative identity, abelian realization).** The controller's thirty-two bank rows are replayed in the free commutative Laurent ring on `Q` and `D_1, ..., D_33` (the semantics of @@ -98,4 +112,4 @@ Reynolds-type relation and the scalar phase trap vanish at width one and fail at reports three and two distinct elements; exponent two is one element written two ways and vanishes at widths one to three; reversed noncommuting factors are distinct elements and already differ at width one. [test_verify.py](test_verify.py) rejects: input drift, a wrapper phase mutation, a mixed-convention reading, a leftover native warp in the body -endpoint, an owned field left nonzero, overlapping private planes, a missing `Q_POWER`, and a tampered result. +endpoint, a cache SWAP that drops the cache row, a sign change in one mode output word, an owned field left nonzero, overlapping private planes, a missing `Q_POWER`, and a tampered result. diff --git a/research/allwidth-caller-certificate/README.md b/research/allwidth-caller-certificate/README.md index 15946214c7..f842a9998e 100644 --- a/research/allwidth-caller-certificate/README.md +++ b/research/allwidth-caller-certificate/README.md @@ -25,7 +25,7 @@ which `clifford_exact.py` does (Pauli tableau plus the image of `|0>`, fixing th | Layer | Identity | Count | Lifts because | |---|---|---|---| | Ports | `x->X = D`, `y->Y = D`, `y->X = D C_0`, `Q_p = C_0`, both orientations, absolute phase | 896 | group identities | -| Body | free-word endpoint of `NEUTRAL-BACKWARD-v16c` with `PROVIDER_5402` expanded: all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under exact signed alias monomials (318 pure phases, 82 with address action) in their recorded exit frames, 8 mode outputs `C8 (h - Z y)`, 17 owned fields zero | 649 rows | free-word identity | +| Body | free-word endpoint of `NEUTRAL-BACKWARD-v16c` with `PROVIDER_5402` expanded: all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under exact signed alias monomials (318 pure phases, 82 with address action) in their recorded exit frames, 17 owned fields zero; the 8 mode outputs are `C8 z`: their 448 cached provider `y` terms cancel the 448 `y` terms through `C8` element by element | 649 rows | free-word identity; modes in `C[G]` | | Controller | Laurent replay in free commuting `Q, D_1..D_33` reproduces the diagonal; 18 private planes disjoint and disjoint from axis 0; `C_0^2 = X_0`, `C_0^-1 X_0 = C_0`, `[C_0, D] = 0` exact | 32 banks | commutative identity, abelian realization | Backward uses the entrywise-conjugate semantics of PR5376 `PROVIDER.md`. Reading the backward wrappers against @@ -35,7 +35,8 @@ of the certificate. Controls on dense `Q(i)` matrices: the Reynolds-type relation `C_0 = (1+i)/2 I + (1-i)/2 X_0` and the scalar trap `i = iI` vanish at width 1 and fail at width 2 while the census counts three and two distinct elements; exponent two (`C_0^2 = X_0`) is one element and lifts; reversed noncommuting factors differ already at width 1. -[test_verify.py](test_verify.py) rejects eight mutations. +[test_verify.py](test_verify.py) rejects ten mutations, including a cache SWAP that drops the cache row (the error of +an earlier version, found in the review of this PR) and a sign change in one mode output word. ## Reproduce diff --git a/research/allwidth-caller-certificate/RESULT.json b/research/allwidth-caller-certificate/RESULT.json index 2671daaf46..728a038843 100644 --- a/research/allwidth-caller-certificate/RESULT.json +++ b/research/allwidth-caller-certificate/RESULT.json @@ -7,12 +7,18 @@ "helper_alias_pairs_pure_phase": 318, "helper_alias_pairs_with_address_action": 82, "main_rows": "X_p = Nout_x(Nin_x x_p - Nin_y y_p), Y_p = Nout_y Nin_y y_p on all 112 ports", - "mode_outputs": 8, - "mode_terms": 456, + "mode_outputs": { + "cached_terms": 448, + "cancelled_y_pairs": 448, + "free_word_terms": 904, + "output": "C8 z on all 8 modes (positive C8 on axes 0..7, absolute phase)", + "paid_C8_terms": 456, + "y_terms_left": 0 + }, "owned_zero": 17, "warps_cancelled": true }, - "conclusion": "The complete #5413 caller identity is a composition of (i) a free-word identity of the body, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.", + "conclusion": "The complete #5413 caller identity is a composition of (i) a free-word identity of the body whose 8 mode outputs reduce to C8 z in C[G] once the cached provider path and the paid C8 path are bound to exact elements, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.", "controller": { "central_axis": 0, "group_identities": [ diff --git a/research/allwidth-caller-certificate/TASK.json b/research/allwidth-caller-certificate/TASK.json index d3bb4fe686..881316bf02 100644 --- a/research/allwidth-caller-certificate/TASK.json +++ b/research/allwidth-caller-certificate/TASK.json @@ -81,7 +81,7 @@ "budget_minutes": 240, "stop_rule": "Stop at the composite certificate of the selected caller; the physical implementation of lifted operators is a separate (direction 10) question.", "outcome": "completed", - "evidence": "verify.py: 896 exact group identities bind every port path to the controller symbols D and C_0 with absolute phase in both orientations (the mixed orientation convention differs on all 112 ports); the free-word body replay with the #5402 provider expanded ends with every warp cancelled and only the port wrappers on main rows; the controller Laurent replay is a free commutative identity realized on 18 disjoint private planes plus the central axis, with C_0^2 = X_0 and C_0^-1 X_0 = C_0 exact; lemma controls on dense Q(i) matrices show the Reynolds and scalar-phase traps pass width 1 and fail width 2. test_verify.py rejects eight mutations.", + "evidence": "verify.py: 896 exact group identities bind every port path to the controller symbols D and C_0 with absolute phase in both orientations (the mixed orientation convention differs on all 112 ports); the free-word body replay with the #5402 provider expanded ends with every warp cancelled and only the port wrappers on main rows, and the 8 mode outputs are C8 z in C[G] (the 448 cached provider y terms cancel the 448 y terms through C8 with exact phase); the controller Laurent replay is a free commutative identity realized on 18 disjoint private planes plus the central axis, with C_0^2 = X_0 and C_0^-1 X_0 = C_0 exact; lemma controls on dense Q(i) matrices show the Reynolds and scalar-phase traps pass width 1 and fail width 2. test_verify.py rejects ten mutations.", "author": "Mark (Matarener)", "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", "open_questions": [ diff --git a/research/allwidth-caller-certificate/VERIFY.json b/research/allwidth-caller-certificate/VERIFY.json index 11972a44c1..6997e7b8af 100644 --- a/research/allwidth-caller-certificate/VERIFY.json +++ b/research/allwidth-caller-certificate/VERIFY.json @@ -22,7 +22,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Pinned inputs; controller and plan bind the body; 896 exact group identities (112 ports, both orientations, paths x->X = D, y->Y = D, y->X = D C_0, Q_p = C_0 with absolute phase; mixed convention differs on all ports); free-word body endpoint with the #5402 provider expanded (all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under signed alias monomials in their recorded exit frames, 8 mode outputs C8 (h - Z y), 17 owned fields zero); Laurent replay reproduces the diagonal; 18 private planes disjoint from each other and from the central axis; C_0^2 = X_0, C_0^-1 X_0 = C_0, [C_0, D] = 0 exactly; even Q_POWER; 16 negative banks corrected by X; lemma controls on dense Q(i) matrices (Reynolds and scalar-phase traps pass width 1 and fail width 2, exponent two lifts, reversed factors differ); stored RESULT.json equals the rebuild." + "checks": "Pinned inputs; controller and plan bind the body; 896 exact group identities (112 ports, both orientations, paths x->X = D, y->Y = D, y->X = D C_0, Q_p = C_0 with absolute phase; mixed convention differs on all ports); free-word body endpoint with the #5402 provider expanded (all warps cancel, main rows carry only the port wrappers, 400 autonomous helpers under signed alias monomials in their recorded exit frames, cache SWAPs move the cache rows to the mode owners, 8 mode outputs C8 z in C[G] with all 448 y pairs cancelled (the unconjugated reading leaves 896 y terms), 17 owned fields zero); Laurent replay reproduces the diagonal; 18 private planes disjoint from each other and from the central axis; C_0^2 = X_0, C_0^-1 X_0 = C_0, [C_0, D] = 0 exactly; even Q_POWER; 16 negative banks corrected by X; lemma controls on dense Q(i) matrices (Reynolds and scalar-phase traps pass width 1 and fail width 2, exponent two lifts, reversed factors differ); stored RESULT.json equals the rebuild." }, { "argv": [ @@ -32,7 +32,7 @@ "{package}/test_verify.py" ], "timeout_seconds": 600, - "checks": "Rejecting controls: input drift, a wrapper phase mutation, the mixed orientation convention, a leftover native warp at the body endpoint, an owned field not cleared, overlapping private planes, a missing controller Q_POWER, tampered RESULT.json." + "checks": "Rejecting controls: input drift, a wrapper phase mutation, the mixed orientation convention, a leftover native warp at the body endpoint, a cache SWAP that drops the cache row, a sign flip in one mode output word, an owned field not cleared, overlapping private planes, a missing controller Q_POWER, tampered RESULT.json." } ] } diff --git a/research/allwidth-caller-certificate/test_verify.py b/research/allwidth-caller-certificate/test_verify.py index 629cd542a7..6218a16bd6 100644 --- a/research/allwidth-caller-certificate/test_verify.py +++ b/research/allwidth-caller-certificate/test_verify.py @@ -58,6 +58,25 @@ def leftover_warp(): V.body_endpoint(B, V.Ops(CE, CAN, NORM)) +def dropped_cache(): + # the review of #5442: a cache SWAP that discards the transformed cache row instead of moving it + src = (HERE / 'verify.py').read_text(encoding='utf-8') + old, new = 'self.rows[cs], self.rows[o] = self.rows[o], self.rows[cs]', 'self.rows[cs], self.rows[o] = self.rows[o], {}' + V.require(src.count(old) == 1, 'mutation site present') + ns = {'__file__': str(HERE / 'verify.py'), '__name__': 'allwidth_mutant'} + exec(compile(src.replace(old, new), str(HERE / 'verify.py'), 'exec'), ns) + B = ns['Body'](BODY, PROV, WORD, CAN); B.run() + ns['body_endpoint'](B, ns['Ops'](CE, CAN, NORM)) + + +def mode_output_phase(): + prov = copy.deepcopy(PROV) + word = prov['mode_boundaries'][3]['output_N']['literal_word'] + ph = next(e for e in word if e[0] == 'phase'); ph[1] = (ph[1] + 2) % 4 + B = V.Body(BODY, prov, WORD, CAN); B.run() + V.body_endpoint(B, V.Ops(CE, CAN, NORM)) + + def owned_not_cleared(): body = copy.deepcopy(BODY) body['operations'] = [o for o in body['operations'] if o['op'] != 'CLEAR'] @@ -88,6 +107,8 @@ def main(): rejects('wrapper phase mutation (port 7)', wrapper_phase) rejects('mixed orientation convention', mixed_convention) rejects('leftover native warp at the endpoint', leftover_warp) + rejects('cache SWAP that drops the cache row', dropped_cache) + rejects('sign flip in one mode output word', mode_output_phase) rejects('owned field not cleared', owned_not_cleared) rejects('overlapping private planes', overlapping_planes) rejects('missing controller Q_POWER', missing_q_power) diff --git a/research/allwidth-caller-certificate/verify.py b/research/allwidth-caller-certificate/verify.py index d63d4aca47..6657888c26 100644 --- a/research/allwidth-caller-certificate/verify.py +++ b/research/allwidth-caller-certificate/verify.py @@ -274,7 +274,8 @@ def provider(self): cs, o = m['cache_slot'], m['owner'] self.scale(cs, F(m['cache_scalar'])); self.apply(cs, self.newsym('N', o)) require(not self.rows[o], 'mode owner zero before the cache SWAP') - self.rows[cs], self.rows[o] = self.rows[o], {} + self.rows[cs], self.rows[o] = self.rows[o], self.rows[cs] + require(not self.rows[cs] and self.rows[o], 'cache SWAP moves the nonzero cache row to its owner') for f in range(224): self.apply(f, self.newsym('Nout', f)) @@ -333,19 +334,14 @@ def strip_block(wd): require(inp == p + 112 and q == 1 and tuple(s[0] for s in wd) == ('Nin', 'Nout') and B.meaning[wd[0]] == p + 112 and B.meaning[wd[1]] == p + 112, 'Y row is the wrapped y_p') # the 400 autonomous helpers return as their own input under an alias pair of monomials (an exact group - # element pair, inverse to each other); the 8 mode owners return the paid rank-8 Gaussian of h_mode - Z y with - # fixed +-1/2 entries over 56 y inputs (the restored coupled outputs, counted as paid+productive by #5413). - autonomous = 0; alias_pairs_identity = 0; modes = 0; mode_terms = 0 + # element pair, inverse to each other); the 8 mode owners return C8 z (NEUTRAL-PROOF-v16c: S(-DZy + D(Sz+Zy))). + autonomous = 0; alias_pairs_identity = 0 mode_owners = set(B.prov['mode_owners']) + modes = mode_outputs(B, ops, backward=True) + require(mode_outputs(B, ops, backward=False)['y_terms_left'] == 896, 'the unconjugated reading leaves every y term of the modes') for h in range(224, 632): r = B.rows[h] if h in mode_owners: - modes += 1; mode_terms += len(r) - # H = D (h - Z y): own input with coefficient 1 and 56 y inputs with +-1/2 (Z = diag M^T diag / 2), one C8. - require(len(r) == 57 and sum(1 for (inp, wd) in r if inp == h) == 1, 'mode output: own input plus 56 y inputs') - for (inp, wd), q in r.items(): - require((q == 1 if inp == h else 112 <= inp < 224 and abs(q) == F(1, 2)) and [s[0] for s in wd].count('G') == 1, - 'mode output: one paid Gaussian of h_mode - Z y with +-1/2 entries') continue require(len(r) == 1, 'autonomous helper returns one term') (inp, wd), q = next(iter(r.items())) @@ -356,16 +352,76 @@ def strip_block(wd): if m.tab == ops.I.tab: alias_pairs_identity += 1 # identity tableau: a pure central phase i^k autonomous += 1 - require(autonomous == 400 and modes == 8, '400 autonomous helpers, 8 modes') + require(autonomous == 400, '400 autonomous helpers') # the paid climbs of every persistent role telescope to the recorded exit frame (frame changes are inert in rows) require(all(B.frames[i] == B.c['final'][i] for i in range(632)), 'every persistent role ends in its recorded exit frame') return dict(warps_cancelled=True, main_rows='X_p = Nout_x(Nin_x x_p - Nin_y y_p), Y_p = Nout_y Nin_y y_p on all 112 ports', block_monomials_identity=block_maps, exit_frames_recorded=632, autonomous_helpers=400, helper_alias_pairs_pure_phase=alias_pairs_identity, - helper_alias_pairs_with_address_action=400 - alias_pairs_identity, mode_outputs=8, mode_terms=mode_terms, + helper_alias_pairs_with_address_action=400 - alias_pairs_identity, mode_outputs=modes, distinct_warp_symbols=len({abs(e[2]) for e in B.word['word'] if e[0] == 'warp'}), owned_zero=17) +def mode_outputs(B, ops, backward): + """Mode owners in C[G]: every free-word term is bound to its exact group element and like elements are summed. + + Body symbols: M = its literal monomial word, G = the positive C8 on axes 0..7. Provider symbols (the cache path): + Nin_f = input wrapper of f, then the inverse canonical chart of f's entrance frame; N_o = canonical chart of the + recorded mode frame, then the literal output_N word. Charts follow the orientation (backward: entrywise + conjugate), as for the port paths. The 56 cached y terms (provider path, no G) must cancel the 56 y terms of + D(Sz+Zy) (one G) element by element, leaving C8 z with coefficient +1. + """ + ce = ops.ce + C8 = ce.fourier(N9, range(0, 8)) + mb = {m['owner']: m for m in B.prov['mode_boundaries']} + + def wrapper(f): + wr = ops.nz['ports'][f % 112]['compiled_wrappers'] + return wr[('backward_' if backward else '') + ('input_X' if f < 112 else 'input_Y')]['word'] + cache = {} + + def element(wd): + if wd not in cache: + op = ops.I + for s in wd: + t, mean = s[0], B.meaning[s] + if t == 'M': + op = op.then(ops.mono(mean)) + elif t == 'G': + require(mean == 'C_rank8_bits0to7_positive', 'mode Gaussian is the positive C8') + op = op.then(C8) + elif t == 'Nin': + op = op.then(ops.mono(wrapper(mean))).then(ops.chart(B.c['start'][mean], backward).adjoint()) + elif t == 'N': + m = mb[mean] + op = op.then(ops.chart(m['frame'], backward)).then(ops.mono(m['output_N']['literal_word'])) + else: + require(False, 'unexpected symbol on a mode output: ' + t) + cache[wd] = elem(op) + return cache[wd] + terms = cached = paid = left = 0 + for o in B.prov['mode_owners']: + r = B.rows[o] + terms += len(r) + cached += sum(1 for (inp, wd) in r if 'N' in [s[0] for s in wd]) + paid += sum(1 for (inp, wd) in r if [s[0] for s in wd].count('G') == 1) + acc = {} + for (inp, wd), q in r.items(): + k = (inp, element(wd)) + acc[k] = acc.get(k, 0) + q + nz = {k: v for k, v in acc.items() if v} + left += sum(1 for (inp, e) in nz if inp != o) + if backward: + require(len(r) == 113, 'mode owner: 113 free-word terms (own input, 56 paid y terms, 56 cached y terms)') + require(nz == {(o, elem(C8)): 1}, + 'mode output is C8 z: all y contributions cancel in C[G], own input with C8 and coefficient +1') + if backward: + require((terms, cached, paid, left) == (904, 448, 456, 0), 'mode census: 904 terms, 448 cached, 456 through C8, none left') + return dict(free_word_terms=terms, cached_terms=cached, paid_C8_terms=paid, y_terms_left=left, + cancelled_y_pairs=448 if backward else None, + output='C8 z on all 8 modes (positive C8 on axes 0..7, absolute phase)') if backward else dict(y_terms_left=left) + + def laurent(controller): """check_wholecaller_v1 semantics: 32 banks, free commuting Laurent variables Q and D_1..D_33.""" def add(a, b, c=1): @@ -560,7 +616,7 @@ def build(): D = lemma_controls() return dict(lemma='sum_g c_g g^{(x)f} = 0 for all f >= 1 <=> sum_g c_g g = 0 in C[G]; group identities lift by g -> g^{(x)f}', port_bindings=A, body_endpoint=Bres, controller=C, lemma_controls=D, - conclusion='The complete #5413 caller identity is a composition of (i) a free-word identity of the body, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.') + conclusion='The complete #5413 caller identity is a composition of (i) a free-word identity of the body whose 8 mode outputs reduce to C8 z in C[G] once the cached provider path and the paid C8 path are bound to exact elements, (ii) 896 exact group identities binding the ports to C_0 and D, (iii) a free commutative Laurent identity realized by commuting exact elements on disjoint axes. Each lifts to every positive column multiplicity; the algebraic half of native_all_columns holds for this caller. The physical half is not addressed.') def main():