diff --git a/research/transported-frame-caller-price/PROOF.md b/research/transported-frame-caller-price/PROOF.md new file mode 100644 index 0000000000..554639309f --- /dev/null +++ b/research/transported-frame-caller-price/PROOF.md @@ -0,0 +1,80 @@ +# Entrance, terminal, and caller price of one transported frame + +The object is the single warp edit in the PR #3929 recipe: zero-based warp 0 +on lender 243. The entrance basis changes from `(261, 133, 85, 45)` to +`(258, 130, 82, 42, 7)`, and the exit basis changes from `(320, 192, 45, 30)` +to `(320, 192, 42, 25, 7)`. The native map is the original column list. The +36 scalar edits are all in section B. No section A or restore opcode is +edited by the recipe. + +## What the walker charges + +The compiler transcribed in `verify.py` is the PR #3929 `compile_frames` +algorithm: guarded scalar and warp edits, one identity scale on the lender +when the pre-warp frame is a proper subspace of the new entrance, then +cleanup recomputed from the forward word. The histogram is +`audit_core.frame_bill`, the vendored PR #3929 bill. + +On the vendored base word the bill moves only in section B: + +| Piece | Histogram change | +|---|---| +| Entrance identity scale on register 243 | `+1 H1` | +| Positive-climb changes at the 36 edited B indices | `+11 H1 − 4 H3 + 4 H4` | +| Later B climbs whose frames were not themselves edited | `+16 H1 − 16 H2` | +| Section A, centre descents, restore, and final end-climbs | `0` | + +The total is `+28 H1 − 16 H2 − 4 H3 + 4 H4`. Rank mass stays 5134. The width +inventory stays `{4: 26, 5: 2, 6: 18, 7: 53, 8: 96, 9: 213}`. + +## Caller and terminal + +These fields are identical before and after the compile: `ports`, +`start_extra`, `helper_final`, `target_levels`, `cut`, `precondition`, +`compensation`, `centers`, `center_frames`, `initial_corrections`, `A`, +`restore`, `removed`, and `prelude_events`. The caller therefore adds no +child and rewrites no interface. + +Final end-climb counts stay `H1: 289`, `H2: 77`, `H3: 54`. `helper_final` +and every restore opcode and frame stay put. Cleanup gains exactly one +operation, the inverse scale `(scale, 243, 1, 1)` of the entrance identity, +and every other cleanup opcode and frame matches. That inverse is not a +forward frame-bill child. + +## Power tariff + +Let `f(q) = 28 − 16·2^q − 4·3^q + 4·4^q` for real `q`. This is the change in +`Σ n_r r^q` under the histogram delta above. Then `f(0) = 12` and `f(1) = 0`. + +Set `x = 2^q` and `L = log₂ 3`, so `3^q = x^L` and `4^q = x^2`. For +`q ∈ [0, 1]` one has `x ∈ [1, 2]`, and + +`f(q) = 4 g(x)`, `g(x) = 7 − 4x + x^2 − x^L`. + +`g(2) = 3 − 2^L = 0`. Also `2^8 = 256 > 243 = 3^5`, so `L < 8/5`, and +`2^3 = 8 < 9 = 3^2`, so `L > 3/2`. Hence + +`L(L − 1) < (8/5)(3/5) = 24/25 < 2`. + +On `[1, 2]` the exponent `L − 2` is negative, so `x^{L−2} ≤ 1`, with equality +at `x = 1`. Differentiate `h(x) = 2x − L x^{L−1}`: + +`h'(x) = 2 − L(L − 1) x^{L−2} > 2 − 2 = 0`. + +So `h` is strictly increasing and `h(x) ≤ h(2)`. The identity +`2^{L−1} = 3/2` gives `h(2) = 4 − (3/2)L`. The lower bound on `L` gives + +`h(2) < 4 − (3/2)·(3/2) = 7/4 < 4`. + +Therefore `g'(x) = h(x) − 4 < 0` on `[1, 2]`. Since `g(2) = 0`, `g(x) > 0` +on `[1, 2)`, so `f(q) > 0` for every `q ∈ [0, 1)` and `f(1) = 0`. + +Every power tariff `r^q` with `0 ≤ q < 1` therefore prices this frame +strictly above the original word. The zero caller delta and the zero +terminal end-climb delta cannot reverse that sign. Equality holds only for +the rank-mass tariff `q = 1`. + +PR #3933 already shows that the least legal completion of this same entrance +also loses, and that the published non-minimal frames cost less than that +least completion while still losing. This note does not repeat that census. +It prices the published frame's entrance, terminal, and caller separately. diff --git a/research/transported-frame-caller-price/README.md b/research/transported-frame-caller-price/README.md new file mode 100644 index 0000000000..7bc7399ad3 --- /dev/null +++ b/research/transported-frame-caller-price/README.md @@ -0,0 +1,93 @@ +# Transported-frame caller price + +**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 prices the +alternative left by Discussion #1166 comment 19034220 after the moved-ADD pair +was already priced: one compatible transported-native frame under PR #3929, +including entrance, terminal, and caller changes. + +The frame is warp 0 on lender 243 in the published recipe. The entrance basis +goes from `(261, 133, 85, 45)` to `(258, 130, 82, 42, 7)`, and the exit basis +goes from `(320, 192, 45, 30)` to `(320, 192, 42, 25, 7)`. The native map is +unchanged. All 36 scalar edits are in section B. + +On the vendored base word: + +- The entrance charge is one identity scale, `['scale', 243, 1, 1, entrance]`, + at new B index 916. Its own climb is `+1 H1`. The warp position moves from + 916 to 917. +- Caller fields `ports`, `start_extra`, `helper_final`, `target_levels`, + `cut`, `precondition`, `compensation`, `centers`, `center_frames`, + `initial_corrections`, `A`, `restore`, `removed`, and `prelude_events` are + unchanged. The caller adds no child. +- Terminal end-climbs stay `H1: 289`, `H2: 77`, `H3: 54`. Restore is unchanged. + Cleanup gains exactly one inverse scale, `(scale, 243, 1, 1)`, and no other + opcode or frame. +- The forward histogram changes by `+28 H1 − 16 H2 − 4 H3 + 4 H4`: the entrance + scale, `+11 H1 − 4 H3 + 4 H4` at edited B indices, and `+16 H1 − 16 H2` on + later unedited B climbs. Rank mass stays 5134. The width inventory stays + `{4: 26, 5: 2, 6: 18, 7: 53, 8: 96, 9: 213}`. + +[PROOF.md](PROOF.md) shows this delta is strictly positive for every power +tariff `r^q` with `q ∈ [0, 1)`, and zero at the rank-mass tariff `q = 1`. The +zero caller and terminal end-climb deltas cannot reverse that sign. + +PR #3933 already proved that the least legal completion of this entrance also +loses, and that these published non-minimal frames cost less than that +completion while still losing. This package does not repeat the 374-superframe +census. It separates the entrance, terminal, and caller charges that #3933 +left unitemized; that note records no physical caller invoice. + +The base word label is `PR2312-width-exchange-plus-coherent-joint616`. Bytes +are the PR #3929 head `0c0e31cf12e8f4f07e8419a6d33ae85129fb5a01` files +`inputs/BASE-WORD.json.gz`, `inputs/RECIPE.json`, and `vendor/audit_core.py`. +SHA256 pins are checked by `verify.py`. Catalogue provenance is in +[SOURCES.json](SOURCES.json). + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/transported-frame-caller-price +``` + +Direct check: + +```sh +python3.12 -B research/transported-frame-caller-price/verify.py +``` + +Observed marker: + +`PASS_TRANSPORTED_FRAME_CALLER_PRICE 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: 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 warp other than warp 0 have a compatible transported entrance + whose entrance, terminal, and caller bill lowers a power tariff? First + step: one later warp's maximal legal superframe, with the identity scale + and end-climbs charged before native replay. Blocker: the other 71 warps + are not searched 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 recipe, compiler, and base word. +Sagar Thakrar for `audit_core.py`, following Arham Tahir's BORROW-WORD reading. +The word label credits the PR #2312 lineage; dataisfire, PR #3734, is the +staged544 provider context of the handoff. ToikY, PR #3933, for the entrance-cap +obstruction that this note does not re-derive. Chris R / Clear1nsight, discussion +comment 19034220, for the requested three-part 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/transported-frame-caller-price/SOURCES.json b/research/transported-frame-caller-price/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/transported-frame-caller-price/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/transported-frame-caller-price/TASK.json b/research/transported-frame-caller-price/TASK.json new file mode 100644 index 0000000000..ca4d493bf6 --- /dev/null +++ b/research/transported-frame-caller-price/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 one compatible transported frame in the PR #3929 recipe (warp 0 on lender 243), including its entrance scale, terminal end-climbs, and caller-interface fields.", + "scope_change_reason": "The catalogue card asks whether one known scalar simplification improves a paid profile. Discussion #1166 comment 19034220 instead asks for the alternative to the moved-ADD pair: price one compatible transported-native frame under PR #3929, with entrance, terminal, and caller changes. That frame 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 frame's histogram rises on every power tariff below rank mass, while the caller and terminal end-climbs add nothing.", + "budget_minutes": 60, + "stop_rule": "Stop after this one published warp-0 frame. Do not search other entrances, rerun native phases, or reprice PR #3945's owner fill.", + "outcome": "negative-result", + "evidence": "On the vendored PR #3929 base word, the published warp-0 frame inserts one H1 identity scale on register 243, leaves every named caller field and every terminal end-climb count unchanged, and adds exactly one inverse scale to cleanup. The forward histogram changes by +28 H1 -16 H2 -4 H3 +4 H4, rank mass stays 5134, and 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 bill transcription, tariff proof, and write-up.", + "open_questions": [ + { + "question": "Does any later warp, other than warp 0, have a compatible transported entrance whose full entrance-terminal-caller bill lowers a power tariff?", + "why_it_matters": "A single losing warp-0 frame does not close the enlarged search domain PR #3929 opened.", + "first_step": "Freeze one later warp's current entrance and test the unique maximal legal superframe, charging the identity scale, end-climbs, and caller fields before any native replay.", + "blocked_by": "This package prices only the published warp-0 recipe. It does not enumerate the other 71 warps." + }, + { + "question": "Can PR #3945's idle-owner fill absorb this histogram without repaying the +28 H1?", + "why_it_matters": "The width inventory is unchanged, so an owner fill would have to use slots this frame 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/transported-frame-caller-price/VERIFY.json b/research/transported-frame-caller-price/VERIFY.json new file mode 100644 index 0000000000..8eb4c28955 --- /dev/null +++ b/research/transported-frame-caller-price/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/transported-frame-caller-price/inputs/BASE-WORD.json.gz", + "research/transported-frame-caller-price/inputs/RECIPE.json", + "research/transported-frame-caller-price/vendor/audit_core.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Caller-field identity, terminal end-climb identity, one entrance H1 scale, one cleanup inverse scale, histogram split, and the integer hypotheses of the power-tariff obstruction; a swapped exit frame is rejected" + } + ] +} diff --git a/research/transported-frame-caller-price/inputs/BASE-WORD.json.gz b/research/transported-frame-caller-price/inputs/BASE-WORD.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/transported-frame-caller-price/inputs/BASE-WORD.json.gz differ diff --git a/research/transported-frame-caller-price/inputs/RECIPE.json b/research/transported-frame-caller-price/inputs/RECIPE.json new file mode 100644 index 0000000000..b9d2897660 --- /dev/null +++ b/research/transported-frame-caller-price/inputs/RECIPE.json @@ -0,0 +1,731 @@ +{ + "scalar_edits": [ + { + "section": "B", + "index": 916, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 917, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 918, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 919, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 920, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 921, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 922, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 923, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 924, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 925, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 926, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 927, + "old": [ + 320, + 192, + 45, + 30 + ], + "new": [ + 320, + 192, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 928, + "old": [ + 271, + 143, + 79, + 45, + 30 + ], + "new": [ + 264, + 136, + 72, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 929, + "old": [ + 320, + 192, + 41, + 26, + 4 + ], + "new": [ + 320, + 192, + 41, + 25, + 4, + 3 + ] + }, + { + "section": "B", + "index": 930, + "old": [ + 320, + 192, + 44, + 30, + 1 + ], + "new": [ + 320, + 192, + 42, + 24, + 6, + 1 + ] + }, + { + "section": "B", + "index": 931, + "old": [ + 266, + 138, + 74, + 45, + 30 + ], + "new": [ + 266, + 138, + 74, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 932, + "old": [ + 262, + 134, + 70, + 45, + 30 + ], + "new": [ + 257, + 129, + 65, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 933, + "old": [ + 320, + 192, + 32, + 19, + 13 + ], + "new": [ + 320, + 192, + 32, + 19, + 10, + 7 + ] + }, + { + "section": "B", + "index": 934, + "old": [ + 320, + 192, + 37, + 22, + 8 + ], + "new": [ + 320, + 192, + 34, + 17, + 8, + 7 + ] + }, + { + "section": "B", + "index": 935, + "old": [ + 259, + 131, + 67, + 45, + 30 + ], + "new": [ + 259, + 131, + 67, + 42, + 25, + 7 + ] + }, + { + "section": "B", + "index": 1421, + "old": [ + 263, + 135, + 71, + 37, + 22, + 8 + ], + "new": [ + 256, + 128, + 64, + 34, + 17, + 8, + 7 + ] + }, + { + "section": "B", + "index": 1422, + "old": [ + 263, + 135, + 71, + 37, + 22, + 8 + ], + "new": [ + 256, + 128, + 64, + 34, + 17, + 8, + 7 + ] + }, + { + "section": "B", + "index": 1425, + "old": [ + 259, + 131, + 67, + 41, + 26, + 4 + ], + "new": [ + 256, + 128, + 64, + 41, + 25, + 4, + 3 + ] + }, + { + "section": "B", + "index": 1426, + "old": [ + 259, + 131, + 67, + 41, + 26, + 4 + ], + "new": [ + 256, + 128, + 64, + 41, + 25, + 4, + 3 + ] + }, + { + "section": "B", + "index": 1429, + "old": [ + 262, + 134, + 70, + 44, + 30, + 1 + ], + "new": [ + 256, + 128, + 64, + 42, + 24, + 6, + 1 + ] + }, + { + "section": "B", + "index": 1430, + "old": [ + 262, + 134, + 70, + 44, + 30, + 1 + ], + "new": [ + 256, + 128, + 64, + 42, + 24, + 6, + 1 + ] + }, + { + "section": "B", + "index": 1433, + "old": [ + 263, + 135, + 71, + 32, + 19, + 13 + ], + "new": [ + 256, + 128, + 64, + 32, + 19, + 10, + 7 + ] + }, + { + "section": "B", + "index": 1434, + "old": [ + 263, + 135, + 71, + 32, + 19, + 13 + ], + "new": [ + 256, + 128, + 64, + 32, + 19, + 10, + 7 + ] + }, + { + "section": "B", + "index": 1437, + "old": [ + 259, + 131, + 67, + 33, + 18, + 12 + ], + "new": [ + 259, + 131, + 67, + 33, + 18, + 11, + 7 + ] + }, + { + "section": "B", + "index": 1438, + "old": [ + 259, + 131, + 67, + 33, + 18, + 12 + ], + "new": [ + 259, + 131, + 67, + 33, + 18, + 11, + 7 + ] + }, + { + "section": "B", + "index": 1441, + "old": [ + 320, + 192, + 33, + 18, + 8, + 4 + ], + "new": [ + 320, + 192, + 33, + 17, + 8, + 4, + 3 + ] + }, + { + "section": "B", + "index": 1442, + "old": [ + 320, + 192, + 33, + 18, + 8, + 4 + ], + "new": [ + 320, + 192, + 33, + 17, + 8, + 4, + 3 + ] + }, + { + "section": "B", + "index": 1445, + "old": [ + 320, + 192, + 32, + 18, + 12, + 1 + ], + "new": [ + 320, + 192, + 32, + 18, + 10, + 6, + 1 + ] + }, + { + "section": "B", + "index": 1446, + "old": [ + 320, + 192, + 32, + 18, + 12, + 1 + ], + "new": [ + 320, + 192, + 32, + 18, + 10, + 6, + 1 + ] + }, + { + "section": "B", + "index": 1449, + "old": [ + 262, + 134, + 70, + 33, + 18, + 12 + ], + "new": [ + 257, + 129, + 65, + 33, + 18, + 11, + 7 + ] + }, + { + "section": "B", + "index": 1450, + "old": [ + 262, + 134, + 70, + 33, + 18, + 12 + ], + "new": [ + 257, + 129, + 65, + 33, + 18, + 11, + 7 + ] + } + ], + "warp_edits": [ + { + "index": 0, + "old": [ + [ + 261, + 133, + 85, + 45 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "new": [ + [ + 258, + 130, + 82, + 42, + 7 + ], + [ + 320, + 192, + 42, + 25, + 7 + ] + ] + } + ] +} diff --git a/research/transported-frame-caller-price/vendor/NOTICE.md b/research/transported-frame-caller-price/vendor/NOTICE.md new file mode 100644 index 0000000000..3b657f9b2a --- /dev/null +++ b/research/transported-frame-caller-price/vendor/NOTICE.md @@ -0,0 +1,9 @@ +`audit_core.py` is copied unchanged from PR #3929 head +`0c0e31cf12e8f4f07e8419a6d33ae85129fb5a01`, path +`research/transported-warp-frames/vendor/audit_core.py`. + +That module's header credits Sagar Thakrar (thakrarsagar), with Claude +assistance, and records that its frame-bill reading follows Arham Tahir's +`research/coupled-carrier-independent-audit/verify.py`. Apache-2.0. This +package does not modify the file and does not treat the copy as a new audit +of the BORROW-WORD contract. diff --git a/research/transported-frame-caller-price/vendor/audit_core.py b/research/transported-frame-caller-price/vendor/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/transported-frame-caller-price/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/transported-frame-caller-price/verify.py b/research/transported-frame-caller-price/verify.py new file mode 100644 index 0000000000..12ea374c32 --- /dev/null +++ b/research/transported-frame-caller-price/verify.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +"""Price one PR #3929 transported frame: entrance, terminal, and caller. + +The frame bill is the vendored PR #3929 module. The compiler below is the +published compile_frames algorithm, transcribed so this file does not import +research/transported-warp-frames/frames.py. No new kappa is claimed. +""" +import copy +import gzip +import hashlib +import json +from collections import Counter, defaultdict +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE / "vendor")) +import audit_core as audit # noqa: E402 + +BASE_SHA256 = "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699" +RECIPE_SHA256 = "465166937e5c92e6eec1b4b481fc54b689e13e958ad75d0628756c4ea171bc9f" +BILL_SHA256 = "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951" +ENTRANCE = [258, 130, 82, 42, 7] +OLD_ENTRANCE = [261, 133, 85, 45] +EXIT = [320, 192, 42, 25, 7] +OLD_EXIT = [320, 192, 45, 30] +CALLER_FIELDS = ( + "ports", "start_extra", "helper_final", "target_levels", "cut", + "precondition", "compensation", "centers", "center_frames", + "initial_corrections", "A", "restore", "removed", "prelude_events", +) +OLD_PROFILE = {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8} +NEW_PROFILE = {1: 2468, 2: 709, 3: 220, 4: 106, 5: 20, 8: 8} +INVENTORY = {4: 26, 5: 2, 6: 18, 7: 53, 8: 96, 9: 213} +END_CLIMBS = {1: 289, 2: 77, 3: 54} + + +def need(ok, why): + if not ok: + raise SystemExit("FAIL: " + why) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load(): + base_path = PACKAGE / "inputs" / "BASE-WORD.json.gz" + recipe_path = PACKAGE / "inputs" / "RECIPE.json" + bill_path = PACKAGE / "vendor" / "audit_core.py" + need(sha256(base_path) == BASE_SHA256, "base word bytes") + need(sha256(recipe_path) == RECIPE_SHA256, "recipe bytes") + need(sha256(bill_path) == BILL_SHA256, "frame-bill bytes") + with gzip.open(base_path, "rt", encoding="utf-8") as handle: + word = json.load(handle) + recipe = json.loads(recipe_path.read_text(encoding="utf-8")) + return word, recipe + + +def compile_frames(source, recipe): + """PR #3929 compile_frames, including the paid entrance scale.""" + word = copy.deepcopy(source) + seen = set() + for edit in recipe["scalar_edits"]: + section, index = edit["section"], edit["index"] + need(section in ("A", "B", "restore"), "invalid scalar section") + need((section, index) not in seen, "duplicate scalar edit") + seen.add((section, index)) + gate = word[section][index] + need(gate[0] != "warp" and gate[-1] == edit["old"], "scalar source guard") + gate[-1] = list(edit["new"]) + warp_edits = {} + for edit in recipe["warp_edits"]: + index = edit["index"] + need(index not in warp_edits, "duplicate warp edit") + need(source["warps"][index][3:] == edit["old"], "warp source guard") + warp_edits[index] = edit["new"] + current = {register: audit.span((point,)) for register, point in enumerate(word["ports"])} + current.update({register: audit.ZERO for register in range(audit.V, audit.N)}) + for register, frame in word["start_extra"].items(): + current[int(register)] = audit.span(frame) + for gate in word["A"]: + if gate[0] == "warp": + current[gate[1]] = audit.span(gate[4]) + else: + for register in audit.touched(gate): + current[register] = audit.span(gate[-1]) + levels = {audit.V + int(target): audit.span(frame) for target, frame in word["target_levels"].items()} + for register in word["centers"]: + served = {levels.get(gate[1], audit.ZERO) for gate in word["cut"] if gate[2] == register} + for frame in sorted(served, key=lambda mask: -audit.dim(mask)): + current[register] = frame + at = {} + for index, record in enumerate(source["warps"]): + at.setdefault(record[0], []).append(index) + out = [] + for index in range(len(word["B"]) + 1): + for warp_index in at.get(index, ()): + old = source["warps"][warp_index] + entrance, exit_frame = warp_edits.get(warp_index, old[3:]) + entrance_mask, exit_mask = audit.span(entrance), audit.span(exit_frame) + images = audit.warp_images(old[2]) + need(audit.image_mask(images, entrance_mask) == exit_mask, "incompatible transported frame") + need(current[old[1]] & ~entrance_mask == 0, "warp entrance would shrink") + if current[old[1]] != entrance_mask: + out.append(["scale", old[1], 1, 1, list(entrance)]) + word["warps"][warp_index] = [len(out), old[1], copy.deepcopy(old[2]), list(entrance), list(exit_frame)] + current[old[1]] = exit_mask + if index < len(word["B"]): + gate = word["B"][index] + out.append(gate) + for register in audit.touched(gate): + current[register] = audit.span(gate[-1]) + word["B"] = out + word["cleanup"] = audit.derive_cleanup(word) + audit.hygiene(word) + profile, inventory, chain, _, _ = audit.frame_bill(word, lagrangian=True) + word["report"]["local_profile"] = {str(rank): count for rank, count in profile.items()} + word["report"]["width_inventory"] = {str(width): count for width, count in inventory.items()} + return word, profile, inventory, chain + + +def positive_climbs(chain): + located = defaultdict(list) + for events in chain.values(): + for event in events: + if len(event) == 3 and isinstance(event[0], tuple) and event[1]: + located[event[0]].append(event[1]) + return located + + +def end_climb_counts(chain): + counts = Counter() + for ranks in positive_climbs(chain).items(): + where, values = ranks + if where == ("end",): + counts.update(values) + return dict(counts) + + +def b_climb_rows(chain): + rows = defaultdict(list) + for events in chain.values(): + for event in events: + if len(event) == 3 and isinstance(event[0], tuple) and event[0][0] == "B": + rows[event[0][1]].append(event[1]) + return rows + + +def one_inserted_scale(old, new, opcode): + 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 tuple(new[new_index][:-1]) == opcode: + found = 1 + new_index += 1 + else: + return False + return found == 1 and old_index == len(old) and new_index == len(new) + + +def histogram_parts(old_rows, new_rows, edit_indices, scale_index): + entrance = Counter() + edited = Counter() + propagated = Counter() + mapped = set() + for index, climbs in old_rows.items(): + new_index = index if index < scale_index else index + 1 + mapped.add(new_index) + before = Counter(rank for rank in climbs if rank) + after = Counter(rank for rank in new_rows.get(new_index, []) if rank) + bucket = edited if index in edit_indices else propagated + for rank in set(before) | set(after): + change = after[rank] - before[rank] + if change: + bucket[rank] += change + extra = set(new_rows) - mapped + need(extra == {scale_index}, "unexpected B climb index " + str(sorted(extra))) + for rank in new_rows[scale_index]: + if rank: + entrance[rank] += 1 + return entrance, edited, propagated + + +def tariff_hypotheses(delta): + """Integer hypotheses of PROOF.md. The sign argument is that prose.""" + need(delta == {1: 28, 2: -16, 3: -4, 4: 4}, "histogram delta") + need(28 - 16 - 4 + 4 == 12, "f(0)") + need(28 - 16 * 2 - 4 * 3 + 4 * 4 == 0, "f(1)") + need(2 ** 8 > 3 ** 5, "log2(3) < 8/5") + need(2 ** 3 < 3 ** 2, "log2(3) > 3/2") + need(8 * 3 < 5 * 5, "L(L-1) < 24/25") + need(24 < 25 * 2, "24/25 < 2") + need(4 * 4 - 9 < 16, "h(2) upper bound 7/4 is below 4") + + +def main(): + word, recipe = load() + need(word["base"] == "PR2312-width-exchange-plus-coherent-joint616", "base label") + need(len(recipe["warp_edits"]) == 1, "one warp edit") + warp = recipe["warp_edits"][0] + need(warp["index"] == 0, "warp index") + need(warp["old"] == [OLD_ENTRANCE, OLD_EXIT], "old frames") + need(warp["new"] == [ENTRANCE, EXIT], "new frames") + need(len(recipe["scalar_edits"]) == 36, "36 scalar edits") + need({edit["section"] for edit in recipe["scalar_edits"]} == {"B"}, "B-only scalar edits") + edit_indices = {edit["index"] for edit in recipe["scalar_edits"]} + need(len(edit_indices) == 36 and 916 in edit_indices, "edit index set") + + old_profile, old_inventory, old_chain, _, _ = audit.frame_bill(word, lagrangian=True) + compiled, new_profile, new_inventory, new_chain = compile_frames(word, recipe) + need(old_profile == OLD_PROFILE and new_profile == NEW_PROFILE, "profiles") + need(old_inventory == new_inventory == INVENTORY, "width inventory") + need(sum(rank * count for rank, count in old_profile.items()) == 5134, "old mass") + need(sum(rank * count for rank, count in new_profile.items()) == 5134, "new mass") + + for field in CALLER_FIELDS: + need(word[field] == compiled[field], "caller field changed: " + field) + need(end_climb_counts(old_chain) == end_climb_counts(new_chain) == END_CLIMBS, "terminal end climbs") + need(compiled["warps"][0][2] == word["warps"][0][2], "native map") + need(len(word["B"]) == 1869 and len(compiled["B"]) == 1870, "B length") + need(sum(gate[0] == "scale" for gate in compiled["B"]) == 74, "one new scale") + need(word["warps"][0][0] == 916 and compiled["warps"][0][0] == 917, "warp position") + need(compiled["B"][916] == ["scale", 243, 1, 1, ENTRANCE], "entrance scale") + need(one_inserted_scale(word["cleanup"], compiled["cleanup"], ("scale", 243, 1, 1)), "cleanup inverse") + + entrance, edited, propagated = histogram_parts( + b_climb_rows(old_chain), b_climb_rows(new_chain), edit_indices, 916) + need(dict(entrance) == {1: 1}, "entrance climb") + need(dict(edited) == {1: 11, 3: -4, 4: 4}, "edited-index climbs") + need(dict(propagated) == {1: 16, 2: -16}, "propagated climbs") + total = Counter() + for part in (entrance, edited, propagated): + for rank, change in part.items(): + total[rank] += change + need(dict(total) == {1: 28, 2: -16, 3: -4, 4: 4}, "parts sum") + tariff_hypotheses(dict(total)) + + # The published exit is the image of the new entrance. A swapped exit is illegal. + broken = copy.deepcopy(recipe) + broken["warp_edits"][0]["new"] = [ENTRANCE, OLD_EXIT] + try: + compile_frames(word, broken) + except SystemExit as exc: + need("incompatible transported frame" in str(exc), "wrong rejection") + else: + need(False, "swapped exit was accepted") + + print( + "PASS_TRANSPORTED_FRAME_CALLER_PRICE " + "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()