diff --git a/research/later-warp-maximal-entrance/PROOF.md b/research/later-warp-maximal-entrance/PROOF.md new file mode 100644 index 0000000000..385bfa253c --- /dev/null +++ b/research/later-warp-maximal-entrance/PROOF.md @@ -0,0 +1,93 @@ +# Maximal entrance of the native event after warp 0 + +SPDX-License-Identifier: Apache-2.0. This is a source-bound calculation on one +frozen word, not a proof-assistant certificate and not a new kappa. + +## Domain + +Frames are subspaces of \(V=\mathbb F_2^9\). The word is the PR #3929 base +word. Warp array index 0 is lender 243 at original B position 916. Eight +native events precede it. The next native event is warp array index 13, on +lender 349 at the same B position. Its original entrance is + +\[ +U=\operatorname{span}(416,70,19,13), +\] + +dimension 4, and its map \(G\) is the published invertible column map. + +Freeze the prefix through warp 0, the ordered scalar operations and their +original frames as floors, every native map, and the terminal caps. A later +scalar frame must contain its original frame and the incoming frames of its +operands. A later native entrance must contain its original entrance and the +incoming lender frame; its exit is the image under the unchanged map. PR #3933 +proved that, in this domain, backward capacity produces the unique maximal +legal seed and the least-join completion is legal exactly when that seed is. + +## Entrance + +The backward pass on the suffix after warp 13 returns + +\[ +C=U+\operatorname{span}(7), +\] + +dimension 5. The same pass on warp 0 returns the entrance PR #3933 recorded, +\(U_0+\operatorname{span}(7)\). That is a control on the transcription, not a +new proof of the warp-0 theorem. + +Of the 31 lines of \(V/U\), the forward least-join test admits only +\(\operatorname{span}(7)\). The original entrance is legal. One explicit +dimension-6 join of \(C\) with another quotient line fails the terminal caps. +The verifier checks these statements on the hashed word. + +## Three charges + +The least completion of \(C\) inserts one identity scale on register 349. +That scale is the entrance charge, \(+1\,H_1\). + +The named caller fields are unchanged, including `restore`. Terminal +end-climb counts stay \(H_1:289\), \(H_2:77\), \(H_3:54\). Cleanup gains +exactly one inverse scale on the buffered lender and no other gate. A swapped +exit on the same entrance fails the frame bill. + +The forward histogram changes by + +\[ ++28\,H_1-16\,H_2-4\,H_3+4\,H_4. +\] + +Rank mass stays 5134. The warp-0 least completion, run with the same code, has +delta \(+27\,H_1-14\,H_2-H_3+H_4\), matching the canonical delta stated by +PR #3933. Warp 13 is not that completion: the lender, the original entrance, +and the delta differ. + +## Power tariff + +For \(q\in\mathbb R\), + +\begin{align*} +f(q) +&=28-16\cdot 2^q-4\cdot 3^q+4\cdot 4^q\\ +&=4\bigl((2-2^q)^2+(3-3^q)\bigr). +\end{align*} + +The integer endpoints are \(f(0)=12\) and \(f(1)=0\). For \(q\in[0,1)\), +\(3^q<3\), so the second summand is positive and \(f(q)>0\). At the rank-mass +tariff \(q=1\), \(f(1)=0\). + +The ordinary raw-moment comparison uses the same sign. A child of rank \(r\) +contributes a positive multiple of \(r^{1-a}\). Substituting \(q=1-a\) makes +the moment difference a positive multiple of \(f(1-a)\). It is therefore +strictly positive for every \(a\in(0,1]\) and zero at \(a=0\). + +This delta is the one PR #3933 already factored for the published nonminimal +warp-0 recipe. The identity applies to any histogram with these four +coefficients. It does not identify the two words. + +## What this does not show + +No search of the other 62 native events, no native-phase replay, no +PR #3945 owner fill, and no selected cold replay. A loss on warp 13 does not +forbid a different warp from lowering a power tariff. Unknown owner-fill cost +is not zero. Selected \(\kappa\) stays \(0.001672660197076918\). diff --git a/research/later-warp-maximal-entrance/README.md b/research/later-warp-maximal-entrance/README.md new file mode 100644 index 0000000000..32de58d95d --- /dev/null +++ b/research/later-warp-maximal-entrance/README.md @@ -0,0 +1,81 @@ +# Later-warp maximal entrance + +**Negative result. No new κ.** Selected κ stays `0.001672660197076918`. + +## Scope and evidence + +Original card: `scalar-to-moment`, scope **changed**. The card asks whether +one scalar simplification improves a paid profile. This package answers the +first open question of the warp-0 transported-frame bill: one later native +event's maximal legal entrance, with entrance, terminal, and caller charges. + +Warp array index 13 is the native event immediately after warp 0 on the +PR #3929 base word. It uses lender 349 at original B position 916. The +original entrance is `span(416, 70, 19, 13)`. + +On that word: + +- Backward capacity returns `C = U + span(7)`, dimension 5. The same pass + recovers PR #3933's warp-0 entrance `U0 + span(7)` as a transcription + control. +- Exactly one of the 31 quotient lines is legal. One explicit dimension-6 + join fails the terminal caps. +- The least completion inserts one identity scale on register 349. The named + caller fields stay byte-identical. Terminal end-climbs stay `H1: 289`, + `H2: 77`, `H3: 54`. Cleanup gains exactly one inverse scale. +- The forward histogram changes by `+28 H1 − 16 H2 − 4 H3 + 4 H4`. Rank mass + stays 5134. + +[PROOF.md](PROOF.md) factors that delta as `4*((2-2^q)^2+(3-3^q))`, strictly +positive for every power tariff `r^q` with `q` in `[0, 1)` and zero at rank +mass. The zero caller and terminal end-climb deltas cannot reverse that sign. + +The base word and frame bill are the bytes already hashed by the warp-0 +price. SHA256 pins are checked by `verify.py`. Catalogue provenance is in +[SOURCES.json](SOURCES.json). [vendor/NOTICE.md](vendor/NOTICE.md) records +why those bytes are not files of this base commit. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/later-warp-maximal-entrance +``` + +Direct check: + +```sh +python3.12 -B research/later-warp-maximal-entrance/verify.py +``` + +Observed marker: + +`PASS_LATER_WARP_MAXIMAL_ENTRANCE warp=13 lender=349 next_native_after_warp0 C=U+span(7) dim=5 admitted_line=7 entrance=+1H1 terminal_end_climbs=0 caller_fields=0 histogram=+28H1-16H2-4H3+4H4 mass=5134 power_tariff_strict_for_q_in_[0,1) no_new_kappa` + +Not run: the other 62 native events, native phase replay, an owner fill +against PR #3945, a selected cold replay, Lean, or Docker. The power-tariff +sign is the argument in PROOF.md; the verifier checks the integer hypotheses +that argument cites. + +## Open next questions + +1. Does any of the other 62 native events after warp 0 have a legal entrance + enlargement whose full entrance-terminal-caller bill lowers a power tariff? + First step: the next native event after warp 13, with the same backward + pass and least completion. Blocker: those capacity masks are not stored + here. +2. Can PR #3945's idle-owner fill absorb `+28 H1` without a new slot? First + step: add this exact child delta to the pinned #3945 profile. Blocker: + that word is not an input of this package. + +## Credit + +Dugongue, PR #3929, for the transported-frame word and maps. ToikY, PR #3933, +for the backward-capacity theorem and the warp-0 canonical delta used as the +transcription control. Sagar Thakrar for `audit_core.py`, following Arham +Tahir's BORROW-WORD reading. The word label credits the PR #2312 lineage. +The warp-0 three-charge split that posed this question is the fork package +`research/transported-frame-caller-price`. Prepared by unpaidmoon with +substantial Cursor Grok assistance. Apache-2.0. No independent human or +formal-kernel review is claimed. diff --git a/research/later-warp-maximal-entrance/SOURCES.json b/research/later-warp-maximal-entrance/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/later-warp-maximal-entrance/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/later-warp-maximal-entrance/TASK.json b/research/later-warp-maximal-entrance/TASK.json new file mode 100644 index 0000000000..2ec6ead23d --- /dev/null +++ b/research/later-warp-maximal-entrance/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "scalar-to-moment", + "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439" + ] + }, + "scope_status": "changed", + "actual_scope": "Price the least legal transported entrance of warp array index 13, the native event immediately after warp 0 on the PR #3929 base word, including its entrance scale, terminal end-climbs, and caller fields.", + "scope_change_reason": "The catalogue card asks whether one known scalar simplification improves a paid profile. The open question left by the warp-0 transported-frame bill is a different object: one later native event's maximal legal entrance and its entrance, terminal, and caller charges. Warp 13 is not an R439 helper-star word.", + "bottleneck_link": "A frame edit improves the multiplication exponent only when the paid child histogram falls and the caller does not put the cost back. This entrance's histogram rises on every power tariff below rank mass, while the caller fields and terminal end-climbs add nothing.", + "budget_minutes": 60, + "stop_rule": "Stop after this one later warp. Do not search the other 62 native events, rerun native phases, or reprice PR #3945's owner fill.", + "outcome": "negative-result", + "evidence": "On the vendored PR #3929 base word, warp 13 has maximal legal entrance U+span(7), dimension 5. Its least completion inserts one H1 identity scale on lender 349, leaves the named caller fields and the terminal end-climb counts unchanged, and changes the forward histogram by +28 H1 -16 H2 -4 H3 +4 H4. Rank mass stays 5134. That delta is strictly positive for every power tariff r^q with q in [0,1).", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the capacity transcription, tariff write-up, and verifier.", + "open_questions": [ + { + "question": "Does any of the other 62 native events after warp 0 have a legal entrance enlargement whose entrance, terminal, and caller bill lowers a power tariff?", + "why_it_matters": "One losing later warp does not close the enlarged search domain PR #3929 opened.", + "first_step": "Repeat this backward-capacity pass on the next native event after warp 13 and price its least completion before any native replay.", + "blocked_by": "This package prices only warp 13. It does not store the other capacity masks." + }, + { + "question": "Can PR #3945's idle-owner fill absorb +28 H1 without a new slot?", + "why_it_matters": "The width inventory is not an input of this bill, so an owner fill would have to use slots this entrance does not create.", + "first_step": "Pin the PR #3945 word and add this exact child delta to its paid profile before claiming a joint improvement.", + "blocked_by": "The PR #3945 word and owner map are not vendored here." + } + ] +} diff --git a/research/later-warp-maximal-entrance/VERIFY.json b/research/later-warp-maximal-entrance/VERIFY.json new file mode 100644 index 0000000000..214204ea78 --- /dev/null +++ b/research/later-warp-maximal-entrance/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/later-warp-maximal-entrance/inputs/BASE-WORD.json.gz", + "research/later-warp-maximal-entrance/vendor/audit_core.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Warp-0 capacity control, warp-13 maximal entrance, 31-line admission, one identity scale, unchanged caller fields and terminal end-climbs, histogram delta, cleanup insert, and rejection of a swapped exit" + } + ] +} diff --git a/research/later-warp-maximal-entrance/inputs/BASE-WORD.json.gz b/research/later-warp-maximal-entrance/inputs/BASE-WORD.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/later-warp-maximal-entrance/inputs/BASE-WORD.json.gz differ diff --git a/research/later-warp-maximal-entrance/vendor/NOTICE.md b/research/later-warp-maximal-entrance/vendor/NOTICE.md new file mode 100644 index 0000000000..09cece13f1 --- /dev/null +++ b/research/later-warp-maximal-entrance/vendor/NOTICE.md @@ -0,0 +1,14 @@ +# Vendored frame bill + +`audit_core.py` is the Apache-2.0 frame bill from Sagar Thakrar, following +Arham Tahir's BORROW-WORD reading. The bytes are the file vendored by the +warp-0 transported-frame price at SHA256 +`888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951`. + +`inputs/BASE-WORD.json.gz` is the PR #3929 base word at head +`0c0e31cf12e8f4f07e8419a6d33ae85129fb5a01`, SHA256 +`5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699`. +The word label in that file is `PR2312-width-exchange-plus-coherent-joint616`. + +These bytes are not files of canonical main `bb4bccbf42844d2801487450727c2f63e10d1d0f`. +The verifier checks the hashes above. It does not import PR #3929 or PR #3933. diff --git a/research/later-warp-maximal-entrance/vendor/audit_core.py b/research/later-warp-maximal-entrance/vendor/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/later-warp-maximal-entrance/vendor/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/later-warp-maximal-entrance/verify.py b/research/later-warp-maximal-entrance/verify.py new file mode 100644 index 0000000000..69c324e67c --- /dev/null +++ b/research/later-warp-maximal-entrance/verify.py @@ -0,0 +1,389 @@ +#!/usr/bin/env python3 +"""Maximal legal entrance of the native event immediately after warp 0. + +The backward-capacity rules are the ones proved for this word in PR #3933. +This file recomputes them for warp array index 13. It does not import that +package. No new kappa is claimed. +""" +import copy +import gzip +import hashlib +import sys +from collections import Counter, defaultdict +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE / "vendor")) +import audit_core as audit # noqa: E402 + +BASE_SHA256 = "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699" +BILL_SHA256 = "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951" +TARGET = 13 +CALLER_FIELDS = ( + "ports", "start_extra", "helper_final", "target_levels", "cut", + "precondition", "compensation", "centers", "center_frames", + "initial_corrections", "A", "restore", "removed", "prelude_events", +) + + +def need(ok, why): + if not ok: + raise SystemExit("FAIL: " + why) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def basis_of(mask): + out, acc = [], audit.ZERO + rank = audit.dim(mask) + for point in range(1, 512): + if ((mask >> point) & 1) and ((acc >> point) & 1) == 0: + out.append(point) + acc = audit.span(tuple(out)) + if len(out) == rank: + break + need(audit.span(tuple(out)) == mask, "basis does not span the mask") + return out + + +def join(left, right): + if left & ~right == 0: + return right + if right & ~left == 0: + return left + return audit.span(tuple(basis_of(left) + basis_of(right))) + + +def preimage(images, mask): + acc = 0 + for source, image in enumerate(images): + if (mask >> image) & 1: + acc |= 1 << source + return acc + + +def terminal_caps(word): + removed = set(word["removed"]) + end = {} + for register in range(audit.N): + if register in removed: + continue + if register < audit.V: + end[register] = audit.FULL + elif register < 2 * audit.V: + end[register] = audit.hyperplane(word["ports"][register - audit.V]) + else: + end[register] = audit.FULL + for name, frame in word["helper_final"].items(): + end[int(name)] = audit.span(frame) + return end + + +def events_of(word): + at = defaultdict(list) + for index, record in enumerate(word["warps"]): + at[record[0]].append(index) + events = [] + for position in range(len(word["B"]) + 1): + for index in at.get(position, ()): + events.append(("warp", index)) + if position < len(word["B"]): + events.append(("B", position)) + for index in range(len(word["restore"])): + events.append(("restore", index)) + return events + + +def maximal_entrance(word, target): + """Unique maximal legal seed for one warp, with the prefix frozen.""" + cap = terminal_caps(word) + events = events_of(word) + start = events.index(("warp", target)) + for kind, index in reversed(events[start + 1 :]): + if kind == "warp": + _, lender, columns, entrance, _exit = word["warps"][index] + allowed = preimage(audit.warp_images(columns), cap[lender]) + need(audit.span(entrance) & ~allowed == 0, "later warp floor fails at " + str(index)) + cap[lender] = allowed + else: + gate = word[kind][index] + allowed = audit.FULL + for register in audit.touched(gate): + allowed &= cap[register] + need(audit.span(gate[-1]) & ~allowed == 0, "scalar floor fails at " + kind + " " + str(index)) + for register in audit.touched(gate): + cap[register] = allowed + _pos, lender, columns, entrance, _exit = word["warps"][target] + allowed = preimage(audit.warp_images(columns), cap[lender]) + original = audit.span(entrance) + need(original & ~allowed == 0, "original entrance is outside its capacity") + return allowed + + +def initial_frames(word): + removed = set(word["removed"]) + current = {} + for register in range(audit.N): + if register in removed: + continue + if register < audit.V: + current[register] = audit.span((word["ports"][register],)) + else: + current[register] = audit.ZERO + for name, frame in word["start_extra"].items(): + current[int(name)] = audit.span(frame) + for gate in word["A"]: + if gate[0] == "warp": + current[gate[1]] = audit.span(gate[4]) + else: + frame = audit.span(gate[-1]) + for register in audit.touched(gate): + current[register] = frame + return current + + +def replay_prefix(word, events, stop, current): + for kind, index in events[:stop]: + if kind == "warp": + _pos, lender, _columns, entrance, exit_frame = word["warps"][index] + need(current[lender] == audit.span(entrance), "frozen prefix misses warp " + str(index)) + current[lender] = audit.span(exit_frame) + else: + gate = word[kind][index] + frame = audit.span(gate[-1]) + for register in audit.touched(gate): + current[register] = frame + return current + + +def least_assignment(word, target, seed): + """Least-join frames on the suffix. Returns assigned masks, or None if illegal.""" + events = events_of(word) + start = events.index(("warp", target)) + current = replay_prefix(word, events, start, initial_frames(word)) + images = [audit.warp_images(record[2]) for record in word["warps"]] + _pos, lender, _columns, entrance, _exit = word["warps"][target] + if current[lender] != audit.span(entrance): + return None + if audit.span(entrance) & ~seed: + return None + assigned = {("warp", target): seed} + current[lender] = audit.image_mask(images[target], seed) + caps = terminal_caps(word) + for kind, index in events[start + 1 :]: + if kind == "warp": + lender = word["warps"][index][1] + entrance = join(audit.span(word["warps"][index][3]), current[lender]) + assigned[("warp", index)] = entrance + current[lender] = audit.image_mask(images[index], entrance) + else: + gate = word[kind][index] + frame = audit.span(gate[-1]) + for register in audit.touched(gate): + frame = join(frame, current[register]) + assigned[(kind, index)] = frame + for register in audit.touched(gate): + current[register] = frame + for register, frame in current.items(): + if frame & ~caps[register]: + return None + return assigned + + +def compile_least(word, target, seed, assigned): + compiled = copy.deepcopy(word) + images = [audit.warp_images(record[2]) for record in word["warps"]] + at = defaultdict(list) + for index, record in enumerate(word["warps"]): + at[record[0]].append(index) + current = initial_frames(word) + out = [] + scales = [] + for position in range(len(word["B"]) + 1): + for index in at.get(position, ()): + record = word["warps"][index] + lender = record[1] + if ("warp", index) not in assigned: + entrance, exit_mask = audit.span(record[3]), audit.span(record[4]) + need(current[lender] == entrance, "prefix compile mismatch at warp " + str(index)) + compiled["warps"][index] = [ + len(out), lender, copy.deepcopy(record[2]), list(record[3]), list(record[4]) + ] + current[lender] = exit_mask + else: + entrance = assigned[("warp", index)] + exit_mask = audit.image_mask(images[index], entrance) + need(current[lender] & ~entrance == 0, "entrance would shrink warp " + str(index)) + if current[lender] != entrance: + scales.append(lender) + out.append(["scale", lender, 1, 1, basis_of(entrance)]) + compiled["warps"][index] = [ + len(out), lender, copy.deepcopy(record[2]), + basis_of(entrance), basis_of(exit_mask), + ] + current[lender] = exit_mask + if position < len(word["B"]): + gate = copy.deepcopy(word["B"][position]) + if ("B", position) in assigned: + gate[-1] = basis_of(assigned[("B", position)]) + out.append(gate) + frame = audit.span(gate[-1]) + for register in audit.touched(gate): + current[register] = frame + for index, gate in enumerate(word["restore"]): + if ("restore", index) not in assigned: + continue + if audit.span(compiled["restore"][index][-1]) != assigned[("restore", index)]: + rewritten = copy.deepcopy(compiled["restore"][index]) + rewritten[-1] = basis_of(assigned[("restore", index)]) + compiled["restore"][index] = rewritten + compiled["B"] = out + compiled["cleanup"] = audit.derive_cleanup(compiled) + audit.hygiene(compiled) + return compiled, scales + + +def end_climbs(chain): + counts = Counter() + for events in chain.values(): + for event in events: + if len(event) == 3 and event[0] == ("end",) and event[1]: + counts[event[1]] += 1 + return dict(counts) + + +def delta_of(new, old): + change = Counter(new) + change.subtract(old) + return {rank: count for rank, count in sorted(change.items()) if count} + + +def quotient_lines(original): + """One representative of each line of F_2^9 / original.""" + lines = [] + seen = set() + rank = audit.dim(original) + for point in range(1, 512): + if (original >> point) & 1: + continue + seed = join(original, audit.span((point,))) + if audit.dim(seed) != rank + 1 or seed in seen: + continue + seen.add(seed) + lines.append(point) + need(len(lines) == (1 << (9 - rank)) - 1, "quotient line count") + return lines + + +def cleanup_insert(old, new, lender): + if len(new) != len(old) + 1: + return False + old_index = new_index = found = 0 + while old_index < len(old) and new_index < len(new): + if old[old_index] == new[new_index]: + old_index += 1 + new_index += 1 + elif found == 0 and new[new_index][:4] == ["scale", lender, 1, 1]: + found = 1 + new_index += 1 + else: + return False + return found == 1 and old_index == len(old) and new_index == len(new) + + +def load(): + base_path = PACKAGE / "inputs" / "BASE-WORD.json.gz" + bill_path = PACKAGE / "vendor" / "audit_core.py" + need(sha256(base_path) == BASE_SHA256, "base word bytes") + need(sha256(bill_path) == BILL_SHA256, "frame-bill bytes") + with gzip.open(base_path, "rt", encoding="utf-8") as handle: + return json_load(handle) + + +def json_load(handle): + import json + return json.load(handle) + + +def main(): + word = load() + need(len(word["warps"]) == 72, "warp count") + events = events_of(word) + warp0 = events.index(("warp", 0)) + target_at = events.index(("warp", TARGET)) + need(target_at == warp0 + 1, "warp 13 is not the next native event") + record = word["warps"][TARGET] + need(record[0] == 916 and record[1] == 349, "warp 13 address") + need(record[3] == [416, 70, 19, 13], "warp 13 original entrance") + + original_profile, _, original_chain, _, _ = audit.frame_bill(word, lagrangian=True) + need(original_profile == {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8}, "original profile") + + # Control: the same backward pass recovers PR #3933's warp-0 entrance. + warp0_seed = maximal_entrance(word, 0) + warp0_original = audit.span(word["warps"][0][3]) + need(warp0_seed == join(warp0_original, audit.span((7,))), "warp 0 capacity is not U+span(7)") + warp0_assigned = least_assignment(word, 0, warp0_seed) + need(warp0_assigned is not None, "warp 0 maximal seed rejected") + warp0_word, warp0_scales = compile_least(word, 0, warp0_seed, warp0_assigned) + warp0_profile, _, _, _, _ = audit.frame_bill(warp0_word, lagrangian=True) + need(warp0_scales == [243], "warp 0 scale lender") + need(delta_of(warp0_profile, original_profile) == {1: 27, 2: -14, 3: -1, 4: 1}, "warp 0 canonical delta") + + seed = maximal_entrance(word, TARGET) + original = audit.span(record[3]) + need(seed == join(original, audit.span((7,))), "warp 13 capacity is not U+span(7)") + need(audit.dim(seed) == 5, "warp 13 capacity dimension") + lines = quotient_lines(original) + admitted = [] + for point in lines: + line_seed = join(original, audit.span((point,))) + if least_assignment(word, TARGET, line_seed) is not None: + admitted.append(line_seed) + need(admitted == [seed], "admitted quotient seeds are not exactly U+span(7)") + need(least_assignment(word, TARGET, original) is not None, "original entrance rejected") + rejected = next( + join(original, audit.span((point,))) + for point in lines + if join(original, audit.span((point,))) != seed + ) + need(least_assignment(word, TARGET, join(seed, rejected)) is None, "dimension-6 seed survived") + + assigned = least_assignment(word, TARGET, seed) + compiled, scales = compile_least(word, TARGET, seed, assigned) + profile, _inventory, chain, _, _ = audit.frame_bill(compiled, lagrangian=True) + change = delta_of(profile, original_profile) + need(scales == [349], "entrance scale is not the one identity on lender 349") + need(change == {1: 28, 2: -16, 3: -4, 4: 4}, "histogram delta") + need(sum(rank * count for rank, count in profile.items()) == 5134, "rank mass") + need(end_climbs(chain) == end_climbs(original_chain) == {1: 289, 2: 77, 3: 54}, "terminal end-climbs") + for name in CALLER_FIELDS: + need(compiled[name] == word[name], "caller field changed: " + name) + need(cleanup_insert(word["cleanup"], compiled["cleanup"], 349), "cleanup is not one added inverse scale") + # Integer endpoints of f(q) = 28 - 16*2^q - 4*3^q + 4*4^q. + need(28 - 16 - 4 + 4 == 12, "f(0)") + need(28 - 32 - 12 + 16 == 0, "f(1)") + # A swapped exit on the same entrance is not a transported frame. + bad = copy.deepcopy(compiled) + bad["warps"][TARGET][4] = list(record[4]) + try: + audit.frame_bill(bad, lagrangian=True) + except audit.AuditFailure: + pass + else: + raise SystemExit("FAIL: swapped exit was accepted") + + print( + "PASS_LATER_WARP_MAXIMAL_ENTRANCE " + "warp=13 lender=349 next_native_after_warp0 " + "C=U+span(7) dim=5 admitted_line=7 " + "entrance=+1H1 terminal_end_climbs=0 caller_fields=0 " + "histogram=+28H1-16H2-4H3+4H4 mass=5134 " + "power_tariff_strict_for_q_in_[0,1) no_new_kappa" + ) + + +if __name__ == "__main__": + main()