diff --git a/research/repeated-controller-margin/PINS.json b/research/repeated-controller-margin/PINS.json new file mode 100644 index 0000000000..b3b9f8154e --- /dev/null +++ b/research/repeated-controller-margin/PINS.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "upstream_repository": "CrocSwap/integer-mult-bounds", + "predecessor_pr": 4623, + "predecessor_head": "fd5d3be12b9d6ee92c8fa089d95bd529c3236563", + "complementary_audit_pr": 4625, + "files": [ + { + "package_path": "inputs/joint-helper-lattice-RESULT.json", + "upstream_path": "research/joint-helper-lattice/RESULT.json", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21", + "bytes": 9199 + }, + { + "package_path": "inputs/BIT-CONTROLLER.json", + "upstream_path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "bytes": 23753 + } + ], + "predecessor_text_sha256": { + "research/controller-border-interface/BUDGET.md": "10c878e928d390c0101900a60b8ab5ec51d62d514c9ad214cd74ca4733389dbd", + "research/controller-border-interface/budget.py": "f91a3de9db55dcfd59bde615eb7049d8a938ee11399a5ceb47bf77d95ed1578a" + }, + "note": "These bytes were copied from the predecessor head and are not present on this checkout's main. budget.py was not executed or imported." +} diff --git a/research/repeated-controller-margin/README.md b/research/repeated-controller-margin/README.md new file mode 100644 index 0000000000..f6ab3fe2ed --- /dev/null +++ b/research/repeated-controller-margin/README.md @@ -0,0 +1,100 @@ +# Repeated whole-controller rank margins + +**Exact negative rank-mass result for one recovery policy. No new κ.** + +## Scope and evidence + +Original card: `independent-moment` (scope key `c6f2494b197df3bc3591`), chooser +nonce `0ce08b5d1986538ef8eca6579708ff16`, track `independent-verification`. +Scope status: **changed**. The checkout's selected moment already has an +independent price in `research/community-frontier1094-audit/INDEPENDENT1094.json`. +The live upstream handoff left a different pricing claim unchecked: the +repeated-evaluation barrier in open +[PR #4623](https://github.com/CrocSwap/integer-mult-bounds/pull/4623) +(`fd5d3be12b9d6ee92c8fa089d95bd529c3236563`). +[PR #4625](https://github.com/CrocSwap/integer-mult-bounds/pull/4625) +checked the idle-mass identity and the tangent bounds, and left this barrier +open. + +The changed controller is charged once for its main outputs and `K>=2` times +for its local helper and paid invoices. At exponent `t=1` the rank-mass margin +is exactly + +| Lane | `h(1)` | Two-evaluation margin | +|---|---:|---| +| Complex, `b=8`, `v=112` | `-1856` | `-1920 p - 3616` | +| BIT, `b=7`, `v=111` | `-1617` | `-1680 p - 3138` | + +Both coefficients are negative, so every pair count `p>=1` and every `K>=2` +is a rank-mass loss. The added-evaluation step itself is a negative affine +form, so `K=2` is the least negative case. At `p=2` the bills are `-7456` and +`-6498`. Crediting those same main outputs twice instead yields `+160` and +`+162`. + +Every positive signed local term lies strictly above the separator (`6` for +complex, `15/2` for BIT), and every negative term lies strictly below it. The +Jensen base is at least `1+b`, which is also above the separator, and the thin +query has rank 1, below it. Under that coefficient hypothesis, +`F(t)/separator^t` is strictly increasing, so negativity at `t=1` implies +negativity for every smaller `t`. The derivative of `a^t` is the standard +calculus fact used by the predecessor; this package checks the hypothesis and +the `t=1` values, and it does not formalize that derivative. A synthetic +profile `5*2^t - 3*4^t` has a positive term below any separator above 4, and +it is negative at `t=1` but positive at `t=0`. + +The local invoices are rebuilt from the vendored predecessor bytes: + +- complex helpers `{4:28, 7:7, 8:47, 9:326}` and paid calls + `{1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}`; +- BIT thick count 18, after removing main targets, whole-idle costs and thin + queries: helpers `{8:439}` and paid calls + `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`. + +Pins, upstream paths and SHA-256 values are in [PINS.json](PINS.json). The +checker does not import or run `budget.py`. + +This is not a supplier admission, a decoder obstruction, a precision bound, or +a change to the selected frontier. Discussion writes from this account are +forbidden (`addDiscussionComment` returned FORBIDDEN). That limitation is +recorded here and was not retried. + +## Reproduce + +Python 3.12, standard library only. `PYTHONOPTIMIZE` was unset. From the +repository root: + +```sh +python3 -B research/repeated-controller-margin/verify.py +python3 -B scripts/research_package.py --package research/repeated-controller-margin +``` + +The direct command prints `PASS_REPEATED_CONTROLLER_RANK_MARGINS`. + +## Checks not run + +The selected cold replay `make frontier1094-verify` was not run. The tangent +enclosures at `C=.006` and `C=.007`, the copied-input decoder, and the +precision lemma in PR #4623 were not rechecked. No proof assistant was run. + +## Open next questions + +1. Does the exact copied-input X decoder in PR #4623 fail every concave moment + on these same invoices? That is the other recovery route left open by + PR #4625. First step: rebuild its claimed per-port query rank `p-1` and + compare the `t=1` mass. Blocked by the absence of that schedule from the + vendored invoices. +2. Can two evaluations share internal paid calls and avoid the single + main-output credit? The margin above charges the main outputs once. First + step: name the shared calls and recompute the `t=1` mass. Blocked because + no shared-call schedule is in the vendored invoices. + +## Credit + +Dillon's PR #4623 states the repeated-evaluation policy and the published +affine margins. Ryanson Jonathan's PR #4625 checked the complementary idle-mass +identity and tangent bounds. The complex invoice is Cinna Davis's joint-helper +lattice record, and the BIT invoice is the query-thinned controller record, at +predecessor head `fd5d3be12b9d6ee92c8fa089d95bd529c3236563`. Apache-2.0. + +Prepared with substantial AI assistance. No coding-agent product is named. +This is not an independent human or formal-kernel review. diff --git a/research/repeated-controller-margin/SOURCES.json b/research/repeated-controller-margin/SOURCES.json new file mode 100644 index 0000000000..432a6073f0 --- /dev/null +++ b/research/repeated-controller-margin/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + } + ] +} diff --git a/research/repeated-controller-margin/TASK.json b/research/repeated-controller-margin/TASK.json new file mode 100644 index 0000000000..6957e0bd80 --- /dev/null +++ b/research/repeated-controller-margin/TASK.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently rebuild the local complex and BIT invoices used by open PR 4623 and certify its repeated whole-controller rank-mass margins at exponent t=1, including the separator hypothesis that extends negativity to every smaller t.", + "scope_change_reason": "The checkout selected moment already has an independent price. The assigned independent-moment card asks for one exact pricing check with source binding and failure controls. On the current upstream board, PR 4625 checked PR 4623's idle-mass identity and tangent bounds but left the repeated-evaluation barrier unchecked. This package answers that narrower pricing claim. It does not reprice the selected kappa.", + "bottleneck_link": "Deleting idle controller stages removes paid rank and cannot be treated as free recovery. The repeated-evaluation bill is one concrete way that recovery can fail before any supplier admission or kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop once the K>=2 rank-mass margins, separator hypothesis, and ownership fault are exact. Do not audit the decoder, the precision lemma, or a new controller.", + "outcome": "completed", + "evidence": "PASS_REPEATED_CONTROLLER_RANK_MARGINS. Complex h(1)=-1856 and K=2 margin -1920p-3616; BIT h(1)=-1617 and K=2 margin -1680p-3138. At p=2 the correct bills are -7456 and -6498, while crediting the main outputs twice yields +160 and +162. A synthetic profile shows negativity at t=1 need not survive smaller t when a positive term lies below the separator.", + "author": "AI-assisted research session", + "ai_assistance": "Substantial AI assistance was used to choose the scope, derive the margins, and write the checker. No coding-agent product is named. This is not an independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does the exact copied-input X decoder in PR 4623 fail every concave moment for the same pinned invoices?", + "why_it_matters": "It is the other priced recovery route left unchecked by PR 4625. A local repeated-evaluation loss does not decide that decoder.", + "first_step": "Rebuild the claimed per-port query rank p-1 from DECODER.md and compare its t=1 rank mass with the same separator argument.", + "blocked_by": "This package vendors only the two invoice files, not the decoder schedule." + }, + { + "question": "Can evaluations share internal paid calls and avoid the single main-output credit?", + "why_it_matters": "The negative margin uses one credit for the copied main outputs. Shared calls are a different policy.", + "first_step": "Name the shared calls and recompute the t=1 mass with those calls charged once.", + "blocked_by": "No shared-call schedule is present in the vendored invoices." + } + ] +} diff --git a/research/repeated-controller-margin/VERIFY.json b/research/repeated-controller-margin/VERIFY.json new file mode 100644 index 0000000000..e6d99cc46f --- /dev/null +++ b/research/repeated-controller-margin/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/repeated-controller-margin/PINS.json", + "research/repeated-controller-margin/inputs/BIT-CONTROLLER.json", + "research/repeated-controller-margin/inputs/joint-helper-lattice-RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Rebuild both local invoices, certify the K>=2 rank-mass margins and separator hypothesis, and reject three semantic controls." + } + ] +} diff --git a/research/repeated-controller-margin/inputs/BIT-CONTROLLER.json b/research/repeated-controller-margin/inputs/BIT-CONTROLLER.json new file mode 100644 index 0000000000..89c400d597 --- /dev/null +++ b/research/repeated-controller-margin/inputs/BIT-CONTROLLER.json @@ -0,0 +1,2175 @@ +{ + "ambient_rank": 127, + "boundaries": { + "boundary_unit_ADDs_per_port": 160, + "coefficient_projectors": { + "12884901889": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1073741824, + 2147483648 + ], + "1367": [ + 1280, + 0, + 1280, + 0, + 1280, + 0, + 1280, + 0, + 1280, + 682, + 0, + 682, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "13958643713": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 268435456, + 536870912, + 0, + 0 + ], + "14227079169": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 67108864, + 134217728, + 0, + 0, + 0, + 0 + ], + "14294188033": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 16777216, + 33554432, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14310965249": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4194304, + 8388608, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14315159553": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1048576, + 2097152, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316208129": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 262144, + 524288, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316470273": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 65536, + 131072, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "14316557655": [ + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 0, + 16384, + 43690, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "21847": [ + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 0, + 20480, + 10922, + 0, + 10922, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "23": [ + 20, + 0, + 20, + 10, + 0, + 10, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "343": [ + 320, + 0, + 320, + 0, + 320, + 0, + 320, + 170, + 0, + 170, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "5463": [ + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 0, + 5120, + 2730, + 0, + 2730, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "7": [ + 5, + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "87": [ + 80, + 0, + 80, + 0, + 80, + 42, + 0, + 42, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "diagonal_monomials": [ + 7, + 7, + 23, + 23, + 87, + 87, + 343, + 343, + 1367, + 1367, + 5463, + 5463, + 21847, + 21847, + 12884901889, + 12884901889, + 13958643713, + 13958643713, + 14227079169, + 14227079169, + 14294188033, + 14294188033, + 14310965249, + 14310965249, + 14315159553, + 14315159553, + 14316208129, + 14316208129, + 14316470273, + 14316470273, + 14316557655, + 14316557655 + ], + "full_coefficient_endpoint_sha256": "0164c424ad261c955e105330fcec5942d9a863d1b6030f70e786f5cdafb2acef", + "left_program": [ + [ + "SWAP", + 30, + 31 + ], + [ + "SWAP", + 21, + 25 + ], + [ + "SWAP", + 20, + 24 + ], + [ + "SWAP", + 19, + 27 + ], + [ + "SWAP", + 18, + 26 + ], + [ + "SWAP", + 17, + 29 + ], + [ + "SWAP", + 16, + 28 + ], + [ + "SWAP", + 15, + 30 + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 10, + 14 + ], + [ + "ADD", + 8, + 14 + ], + [ + "ADD", + 6, + 14 + ], + [ + "ADD", + 4, + 14 + ], + [ + "ADD", + 2, + 14 + ], + [ + "ADD", + 0, + 14 + ], + [ + "SWAP", + 14, + 31 + ], + [ + "ADD", + 30, + 13 + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 8, + 12 + ], + [ + "ADD", + 6, + 12 + ], + [ + "ADD", + 4, + 12 + ], + [ + "ADD", + 2, + 12 + ], + [ + "ADD", + 0, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 30, + 11 + ], + [ + "ADD", + 12, + 11 + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 6, + 10 + ], + [ + "ADD", + 4, + 10 + ], + [ + "ADD", + 2, + 10 + ], + [ + "ADD", + 0, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 30, + 9 + ], + [ + "ADD", + 12, + 9 + ], + [ + "ADD", + 10, + 9 + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 4, + 8 + ], + [ + "ADD", + 2, + 8 + ], + [ + "ADD", + 0, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 30, + 7 + ], + [ + "ADD", + 12, + 7 + ], + [ + "ADD", + 10, + 7 + ], + [ + "ADD", + 8, + 7 + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 2, + 6 + ], + [ + "ADD", + 0, + 6 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 30, + 5 + ], + [ + "ADD", + 12, + 5 + ], + [ + "ADD", + 10, + 5 + ], + [ + "ADD", + 8, + 5 + ], + [ + "ADD", + 6, + 5 + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 0, + 4 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 30, + 3 + ], + [ + "ADD", + 12, + 3 + ], + [ + "ADD", + 10, + 3 + ], + [ + "ADD", + 8, + 3 + ], + [ + "ADD", + 6, + 3 + ], + [ + "ADD", + 4, + 3 + ], + [ + "ADD", + 0, + 2 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 30, + 1 + ], + [ + "ADD", + 12, + 1 + ], + [ + "ADD", + 10, + 1 + ], + [ + "ADD", + 8, + 1 + ], + [ + "ADD", + 6, + 1 + ], + [ + "ADD", + 4, + 1 + ], + [ + "ADD", + 2, + 1 + ] + ], + "left_rows": [ + 5, + 2, + 10, + 20, + 42, + 80, + 170, + 320, + 682, + 1280, + 2730, + 5120, + 10922, + 20480, + 1073741824, + 2147483648, + 268435456, + 536870912, + 67108864, + 134217728, + 16777216, + 33554432, + 4194304, + 8388608, + 1048576, + 2097152, + 262144, + 524288, + 65536, + 131072, + 43690, + 16384 + ], + "right_program": [ + [ + "ADD", + 13, + 31 + ], + [ + "SWAP", + 30, + 31 + ], + [ + "SWAP", + 21, + 25 + ], + [ + "SWAP", + 20, + 24 + ], + [ + "SWAP", + 19, + 27 + ], + [ + "SWAP", + 18, + 26 + ], + [ + "SWAP", + 17, + 29 + ], + [ + "SWAP", + 16, + 28 + ], + [ + "SWAP", + 15, + 31 + ], + [ + "SWAP", + 14, + 30 + ], + [ + "ADD", + 11, + 13 + ], + [ + "ADD", + 15, + 12 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "ADD", + 9, + 11 + ], + [ + "ADD", + 13, + 10 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "ADD", + 7, + 9 + ], + [ + "ADD", + 11, + 8 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "ADD", + 5, + 7 + ], + [ + "ADD", + 9, + 6 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "ADD", + 3, + 5 + ], + [ + "ADD", + 7, + 4 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "ADD", + 0, + 3 + ], + [ + "ADD", + 5, + 2 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "ADD", + 3, + 1 + ] + ], + "right_rows": [ + 2147494569, + 2, + 2147494568, + 6, + 2147494560, + 20, + 2147494528, + 80, + 2147494400, + 320, + 2147493888, + 1280, + 2147491840, + 5120, + 2147483648, + 1073745920, + 268435456, + 536870912, + 67108864, + 134217728, + 16777216, + 33554432, + 4194304, + 8388608, + 1048576, + 2097152, + 262144, + 524288, + 65536, + 131072, + 16384, + 32768 + ] + }, + "diagonal": [ + 7, + 7, + 23, + 23, + 87, + 87, + 343, + 343, + 1367, + 1367, + 5463, + 5463, + 21847, + 21847, + 12884901889, + 12884901889, + 13958643713, + 13958643713, + 14227079169, + 14227079169, + 14294188033, + 14294188033, + 14310965249, + 14310965249, + 14315159553, + 14315159553, + 14316208129, + 14316208129, + 14316470273, + 14316470273, + 14316557655, + 14316557655 + ], + "invoice": { + "main": { + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "127": 222 + }, + "owned_streams_reused_sequentially": 1, + "paid": { + "1": 25479, + "2": 24156, + "3": 1422, + "4": 792, + "5": 1836, + "6": 198, + "7": 342, + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + }, + "paid_calls": 57555, + "productive_fields": 11454, + "rank_surplus": 753, + "raw_scalar_record_bound": 1000000000, + "targets": { + "8": 7902, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "127": 222 + }, + "thick_calls": 18, + "thick_stages": [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ], + "thin_queries": 1665, + "whole_idle": { + "14": 444, + "21": 444, + "28": 444, + "35": 444, + "42": 444, + "49": 444, + "56": 444, + "63": 222 + } + }, + "keep_mask": 35047648968703, + "kind": "bit", + "pairs": 16, + "physical_events": [ + [ + "LOCAL", + 0, + 0, + false + ], + [ + "LOCAL", + 1, + 0, + true + ], + [ + "IDLE", + 1, + [ + 0, + 1 + ] + ], + [ + "ADD", + 0, + 2 + ], + [ + "ADD", + 3, + 1 + ], + [ + "QUERY_SHEAR", + 2, + 0, + false + ], + [ + "ADD", + 0, + 2 + ], + [ + "ADD", + 3, + 1 + ], + [ + "LOCAL", + 3, + 1, + true + ], + [ + "IDLE", + 2, + [ + 0, + 1, + 3 + ] + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 5, + 3 + ], + [ + "QUERY_SHEAR", + 4, + 1, + false + ], + [ + "ADD", + 2, + 4 + ], + [ + "ADD", + 5, + 3 + ], + [ + "LOCAL", + 5, + 2, + true + ], + [ + "IDLE", + 3, + [ + 0, + 1, + 3, + 5 + ] + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 7, + 5 + ], + [ + "QUERY_SHEAR", + 6, + 2, + false + ], + [ + "ADD", + 4, + 6 + ], + [ + "ADD", + 7, + 5 + ], + [ + "LOCAL", + 7, + 3, + true + ], + [ + "IDLE", + 4, + [ + 0, + 1, + 3, + 5, + 7 + ] + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 9, + 7 + ], + [ + "QUERY_SHEAR", + 8, + 3, + false + ], + [ + "ADD", + 6, + 8 + ], + [ + "ADD", + 9, + 7 + ], + [ + "LOCAL", + 9, + 4, + true + ], + [ + "IDLE", + 5, + [ + 0, + 1, + 3, + 5, + 7, + 9 + ] + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 11, + 9 + ], + [ + "QUERY_SHEAR", + 10, + 4, + false + ], + [ + "ADD", + 8, + 10 + ], + [ + "ADD", + 11, + 9 + ], + [ + "LOCAL", + 11, + 5, + true + ], + [ + "IDLE", + 6, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11 + ] + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 13, + 11 + ], + [ + "QUERY_SHEAR", + 12, + 5, + false + ], + [ + "ADD", + 10, + 12 + ], + [ + "ADD", + 13, + 11 + ], + [ + "LOCAL", + 13, + 6, + true + ], + [ + "IDLE", + 7, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13 + ] + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 15, + 13 + ], + [ + "QUERY_SHEAR", + 14, + 6, + false + ], + [ + "ADD", + 12, + 14 + ], + [ + "ADD", + 15, + 13 + ], + [ + "LOCAL", + 15, + 7, + true + ], + [ + "ADD", + 14, + 16 + ], + [ + "ADD", + 17, + 15 + ], + [ + "QUERY_SHEAR", + 16, + 7, + false + ], + [ + "ADD", + 14, + 16 + ], + [ + "ADD", + 17, + 15 + ], + [ + "LOCAL", + 17, + 8, + true + ], + [ + "ADD", + 16, + 18 + ], + [ + "ADD", + 19, + 17 + ], + [ + "QUERY_SHEAR", + 18, + 8, + false + ], + [ + "ADD", + 16, + 18 + ], + [ + "ADD", + 19, + 17 + ], + [ + "LOCAL", + 19, + 9, + true + ], + [ + "ADD", + 18, + 20 + ], + [ + "ADD", + 21, + 19 + ], + [ + "QUERY_SHEAR", + 20, + 9, + false + ], + [ + "ADD", + 18, + 20 + ], + [ + "ADD", + 21, + 19 + ], + [ + "LOCAL", + 21, + 10, + true + ], + [ + "ADD", + 20, + 22 + ], + [ + "ADD", + 23, + 21 + ], + [ + "QUERY_SHEAR", + 22, + 10, + false + ], + [ + "ADD", + 20, + 22 + ], + [ + "ADD", + 23, + 21 + ], + [ + "LOCAL", + 23, + 11, + true + ], + [ + "ADD", + 22, + 24 + ], + [ + "ADD", + 25, + 23 + ], + [ + "QUERY_SHEAR", + 24, + 11, + false + ], + [ + "ADD", + 22, + 24 + ], + [ + "ADD", + 25, + 23 + ], + [ + "LOCAL", + 25, + 12, + true + ], + [ + "ADD", + 24, + 26 + ], + [ + "ADD", + 27, + 25 + ], + [ + "QUERY_SHEAR", + 26, + 12, + false + ], + [ + "ADD", + 24, + 26 + ], + [ + "ADD", + 27, + 25 + ], + [ + "LOCAL", + 27, + 13, + true + ], + [ + "ADD", + 26, + 28 + ], + [ + "ADD", + 29, + 27 + ], + [ + "QUERY_SHEAR", + 28, + 13, + false + ], + [ + "ADD", + 26, + 28 + ], + [ + "ADD", + 29, + 27 + ], + [ + "LOCAL", + 29, + 14, + true + ], + [ + "ADD", + 28, + 30 + ], + [ + "ADD", + 31, + 29 + ], + [ + "QUERY_SHEAR", + 30, + 14, + false + ], + [ + "ADD", + 28, + 30 + ], + [ + "ADD", + 31, + 29 + ], + [ + "LOCAL", + 31, + 15, + true + ], + [ + "LOCAL", + 32, + 15, + false + ], + [ + "IDLE", + 7, + [ + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 8, + [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 9, + [ + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 10, + [ + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 11, + [ + 25, + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 12, + [ + 27, + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 13, + [ + 29, + 31, + 32 + ] + ], + [ + "IDLE", + 14, + [ + 31, + 32 + ] + ], + [ + "ADD", + 30, + 28 + ], + [ + "ADD", + 29, + 31 + ], + [ + "ADD", + 28, + 26 + ], + [ + "ADD", + 27, + 29 + ], + [ + "ADD", + 26, + 24 + ], + [ + "ADD", + 25, + 27 + ], + [ + "ADD", + 24, + 22 + ], + [ + "ADD", + 23, + 25 + ], + [ + "ADD", + 22, + 20 + ], + [ + "ADD", + 21, + 23 + ], + [ + "ADD", + 20, + 18 + ], + [ + "ADD", + 19, + 21 + ], + [ + "ADD", + 18, + 16 + ], + [ + "ADD", + 17, + 19 + ], + [ + "ADD", + 16, + 14 + ], + [ + "ADD", + 15, + 17 + ], + [ + "ADD", + 14, + 12 + ], + [ + "ADD", + 13, + 15 + ], + [ + "ADD", + 12, + 10 + ], + [ + "ADD", + 11, + 13 + ], + [ + "ADD", + 10, + 8 + ], + [ + "ADD", + 9, + 11 + ], + [ + "ADD", + 8, + 6 + ], + [ + "ADD", + 7, + 9 + ], + [ + "ADD", + 6, + 4 + ], + [ + "ADD", + 5, + 7 + ], + [ + "ADD", + 4, + 2 + ], + [ + "ADD", + 3, + 5 + ], + [ + "ADD", + 2, + 0 + ], + [ + "ADD", + 1, + 3 + ], + [ + "SWAP", + 0, + 1 + ], + [ + "SWAP", + 2, + 3 + ], + [ + "SWAP", + 4, + 5 + ], + [ + "SWAP", + 6, + 7 + ], + [ + "SWAP", + 8, + 9 + ], + [ + "SWAP", + 10, + 11 + ], + [ + "SWAP", + 12, + 13 + ], + [ + "SWAP", + 14, + 15 + ], + [ + "SWAP", + 16, + 17 + ], + [ + "SWAP", + 18, + 19 + ], + [ + "SWAP", + 20, + 21 + ], + [ + "SWAP", + 22, + 23 + ], + [ + "SWAP", + 24, + 25 + ], + [ + "SWAP", + 26, + 27 + ], + [ + "SWAP", + 28, + 29 + ], + [ + "SWAP", + 30, + 31 + ] + ], + "prefix_pairs": 7 +} diff --git a/research/repeated-controller-margin/inputs/joint-helper-lattice-RESULT.json b/research/repeated-controller-margin/inputs/joint-helper-lattice-RESULT.json new file mode 100644 index 0000000000..edf41a49a0 --- /dev/null +++ b/research/repeated-controller-margin/inputs/joint-helper-lattice-RESULT.json @@ -0,0 +1,274 @@ +{ + "compiler": { + "H": 64215200000000, + "N": "2^64215200000000", + "eta": { + "lower": "0.000000206231977820868640096499", + "upper": "0.000000206231977820868640096500" + }, + "gap": "1/1400000000", + "integer_test_exponent": 45868, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "528527/175000000", + "word_materialized": false + }, + "fixed_profile_ceiling": { + "decreasing_through_C": "1/20", + "headroom": [ + "15977/1000000000000", + "159771/10000000000000" + ], + "negative_derivative_upper": { + "lower": "-195970.145588045890401261885812812963", + "upper": "-195970.145588045890401261885812812962" + }, + "remaining_interval_moment_upper": { + "lower": "-6847.019825166589746262304732988153", + "upper": "-6847.019825166589746262304732988152" + }, + "root": [ + "3020165977/1000000000000", + "30201659771/10000000000000" + ] + }, + "full_calls": 18, + "gain_over_PR4416": "4171/12500000", + "gain_over_PR4440": "1203/20000000", + "gain_over_PR4441": "191/10000000", + "gain_over_PR4447": "473/25000000", + "kappa": "60403/20000000", + "kappa_decimal": "0.00302015", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2237, + "2": 388, + "3": 494, + "4": 147, + "5": 36, + "8": 8 + }, + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT": [ + "actual_bit_above_effective" + ], + "unfunded_endpoint": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "nonrecursive": { + "local_route_bound": 4814000, + "local_scalar_allowance": 158168, + "raw_budget": 1000000000, + "raw_upper": 181098496 + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "5919499595771787/1960000000000000000", + "fused_gaussian": "5919499587315361/1960000000000000000", + "global_coordinate_router": "2114107/700000000", + "group_bit_router": "2959750493657679/980000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "5919498195771787/1960000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "802169499595771787/1960000000000000000" + }, + "parameters": { + "a": "2114107/700000000", + "b": "845643/280000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "1782169498195771787/1960000000000000000", + "complex_uniform_saving": "528527/175000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "60403/20000000", + "lambda_": "398791939/400000000", + "lambda_prime": "1395771787/1400000000", + "layout": "1/1400000000", + "q": "4228213/1400000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "604031/200000000" + }, + "strict_checks": { + "actual_bit_above_effective": "265893/700000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "177830503904228213/980000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "5595771787/1960000000000000000", + "cap_above_band": "802169498195771787/1960000000000000000", + "cap_below_cell": "177830500404228213/1960000000000000000", + "cap_below_phase_cell_power": "2137830501804228213/1960000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "7904357/280000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5587315361/1960000000000000000", + "gaussian_above_main": "695771787/980000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "3493657679/980000000000000000", + "group_gauge_power_slack": "177830503834228213/980000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "348942947/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "644589790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "559154357/392000000000000000", + "leaf_saving_above_effective": "279154357/392000000000000000", + "main_transform_above_kappa": "4195771787/1960000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "53897885897/700000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "1395771789/1400000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "559154357/392000000000000000", + "q_positive": "4228213/1400000000", + "short_record_fallback": "279154357/280000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "796250005595771787/1960000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 41946, + "16": 448, + "2": 6984, + "24": 448, + "3": 8892, + "32": 448, + "4": 2646, + "40": 448, + "48": 448, + "5": 648, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "paid_calls": 64620, + "pairs": 16, + "prefix_pairs": 7, + "productive_fields": 10928, + "query_shears": 15, + "scope": "Author-checked conditional construction; retained native/all-column, owned-erasure, whole-job, analytic, precision, tape, prime and recovery contracts. No selected promotion or formal/human acceptance.", + "source_heads": { + "PR4440": "40e22a83ed660d3d6074c4f2dbf14bfb621eee51", + "PR4441_combination": "5f9d871c6bd1b9e34db5a7ea5ef08a908e94db39", + "PR4447": "322e0ec764aa7ef7801383feb1f656e460dd8bed", + "helper_retiming": "ccdae89b2ab9ced24ee3e7adfdb670ef80d223d9" + }, + "source_inputs": 51, + "status": "PASS_CONDITIONAL_JOINT_HELPER_KAPPA_00302015", + "strictification": { + "alpha": { + "lower": "0.999999988558808354139963023136", + "upper": "0.999999988558808354139963023137" + }, + "cutoff": 20, + "delta": { + "lower": "0.958284435309221389866479909583", + "upper": "0.958284435309221389866479909584" + }, + "floor": 21, + "gamma": { + "lower": "0.956176646497545264598139374323", + "upper": "0.956176646497545264598139374324" + }, + "limits": [ + "999999999/1000000000", + "97/100", + "97/100" + ], + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "604031/200000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5868 + }, + "uniform_local_gain": { + "coefficients": { + "1": 17, + "2": 126, + "3": -50, + "4": -42, + "5": 2, + "7": -22, + "8": 5, + "9": 17 + }, + "derivative_upper": { + "lower": "-16.327581880492435373215953558618", + "upper": "-16.327581880492435373215953558617" + }, + "intervals": 128, + "vanishes_at_one": true + } +} diff --git a/research/repeated-controller-margin/verify.py b/research/repeated-controller-margin/verify.py new file mode 100644 index 0000000000..ba1459abc6 --- /dev/null +++ b/research/repeated-controller-margin/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact repeated-evaluation rank margins for the idle-deleted controller model. + +The arithmetic is independent of research/controller-border-interface/budget.py. +It rebuilds the local invoices from the vendored predecessor bytes, then checks +the K>=2 rank-mass claim in that package's BUDGET.md. No kappa is computed. +""" +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +SEPARATOR = {"complex": Fraction(6), "BIT": Fraction(15, 2)} +LANE = {"complex": (8, 112), "BIT": (7, 111)} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load(name): + return json.loads((PACKAGE / "inputs" / name).read_text()) + + +def rank_mass(profile): + return sum(rank * count for rank, count in profile.items()) + + +def signed_counts(helpers, paid): + ranks = set(helpers) | set(paid) + signed = {rank: helpers.get(rank, 0) - paid.get(rank, 0) for rank in ranks} + return {rank: count for rank, count in signed.items() if count} + + +def local_invoices(): + complex_result = load("joint-helper-lattice-RESULT.json") + invoice = load("BIT-CONTROLLER.json")["invoice"] + helpers = {int(rank): count for rank, count in complex_result["local_helpers"].items()} + paid = {int(rank): count for rank, count in complex_result["local_paid"].items()} + need(all(count > 0 for count in (*helpers.values(), *paid.values())), + "complex invoice counts") + full = invoice["thick_calls"] + need(isinstance(full, int) and full > 0, "thick call count") + target = Counter({int(rank): count for rank, count in invoice["targets"].items()}) + cost = Counter({int(rank): count for rank, count in invoice["paid"].items()}) + target.subtract({int(rank): count for rank, count in invoice["main"].items()}) + cost.subtract({int(rank): count for rank, count in invoice["whole_idle"].items()}) + cost[1] -= invoice["thin_queries"] + pieces = [*target.values(), *cost.values()] + need(all(count >= 0 and count % full == 0 for count in pieces), + "BIT local profile does not divide evenly") + bit_helpers = {rank: count // full for rank, count in target.items() if count} + bit_paid = {rank: count // full for rank, count in cost.items() if count} + return { + "complex": {"helpers": helpers, "paid": paid}, + "BIT": {"helpers": bit_helpers, "paid": bit_paid}, + } + + +def separation(signed, separator): + positive = [rank for rank, count in signed.items() if count > 0] + negative = [rank for rank, count in signed.items() if count < 0] + need(positive and negative, "both sides of the local invoice are present") + need(all(rank > separator for rank in positive), "positive term at or below separator") + need(all(rank < separator for rank in negative), "negative term at or above separator") + return positive, negative + + +def main_mass(port_count, stage_factor, pairs): + return 2 * port_count * (pairs + stage_factor * (pairs + 2)) + + +def evaluation_step(pairs, helper_minus_paid, port_count): + """One extra whole-controller evaluation at t=1, after one main credit.""" + return (pairs + 2) * helper_minus_paid - port_count * (pairs - 1) + + +def repeated_margin(pairs, evaluations, helper_minus_paid, port_count, stage_factor): + return (main_mass(port_count, stage_factor, pairs) + + evaluations * evaluation_step(pairs, helper_minus_paid, port_count)) + + +def doubled_main(pairs, evaluations, helper_minus_paid, port_count, stage_factor): + """Ownership fault: credit the same main outputs twice.""" + return (repeated_margin(pairs, evaluations, helper_minus_paid, port_count, stage_factor) + + main_mass(port_count, stage_factor, pairs)) + + +def monotone_hypothesis(signed, separator, stage_factor): + separation(signed, separator) + # For every positive integer pair count the Jensen base is 1+b+2b/p > 1+b. + floor_base = 1 + stage_factor + need(floor_base > separator > 1, "Jensen base or thin query misses the separator") + return floor_base + + +def separated_implication_fails_without_hypothesis(): + """Positive mass below the separator can rise while t falls. + + F(t) = 5*2^t - 3*4^t. Then F(1) < 0 < F(0), so negativity at t=1 does + not imply negativity at every smaller t. + """ + def value(t): + return 5 * (2 ** t) - 3 * (4 ** t) + need(value(1) < 0 < value(0), "synthetic separated-implication control") + return {"t0": value(0), "t1": value(1)} + + +def reject(name, callback): + try: + callback() + except ValueError: + return name + raise ValueError("accepted control: " + name) + + +def controls(invoices): + rejected = [] + complex_helpers = dict(invoices["complex"]["helpers"]) + complex_helpers[9] += 1 + signed = signed_counts(complex_helpers, invoices["complex"]["paid"]) + rejected.append(reject( + "extra_rank9_changes_complex_mass", + lambda: need(rank_mass(signed) == -1856, "mass changed"), + )) + bad = {4: 1, 8: -1} + rejected.append(reject( + "positive_term_below_separator", + lambda: separation(bad, Fraction(6)), + )) + rejected.append(reject( + "indivisible_bit_target", + lambda: bit_profile_or_fail({"targets": {"8": 1}, "paid": {"1": 18}, + "main": {}, "whole_idle": {}, + "thin_queries": 0, "thick_calls": 18}), + )) + return rejected + + +def bit_profile_or_fail(invoice): + full = invoice["thick_calls"] + target = Counter({int(rank): count for rank, count in invoice["targets"].items()}) + cost = Counter({int(rank): count for rank, count in invoice["paid"].items()}) + target.subtract({int(rank): count for rank, count in invoice["main"].items()}) + cost.subtract({int(rank): count for rank, count in invoice["whole_idle"].items()}) + cost[1] -= invoice["thin_queries"] + need(all(count >= 0 and count % full == 0 for count in (*target.values(), *cost.values())), + "BIT local profile does not divide evenly") + + +def lane_report(name, invoice): + stage_factor, port_count = LANE[name] + signed = signed_counts(invoice["helpers"], invoice["paid"]) + helper_minus_paid = rank_mass(signed) + floor_base = monotone_hypothesis(signed, SEPARATOR[name], stage_factor) + step_slope = evaluation_step(1, helper_minus_paid, port_count) - evaluation_step(0, helper_minus_paid, port_count) + # evaluation_step(p) = (p+2)*h - v*(p-1) = (h-v)*p + (2h+v) + step_constant = evaluation_step(0, helper_minus_paid, port_count) + need(step_slope < 0 and step_constant < 0, "each added evaluation is a negative affine form") + margin_slope = 2 * port_count * (1 + stage_factor) + 2 * step_slope + margin_constant = 4 * port_count * stage_factor + 2 * step_constant + need(margin_slope < 0 and margin_constant < 0, "K=2 margin is negative for every positive pair count") + for pairs in range(1, 9): + for evaluations in range(2, 5): + margin = repeated_margin(pairs, evaluations, helper_minus_paid, port_count, stage_factor) + need(margin == main_mass(port_count, stage_factor, pairs) + evaluations * evaluation_step( + pairs, helper_minus_paid, port_count), "margin expansion") + need(margin < 0, "finite repeated margin") + need(margin == (margin_slope * pairs + margin_constant) + + (evaluations - 2) * evaluation_step(pairs, helper_minus_paid, port_count), + "closed form") + fault = doubled_main(2, 2, helper_minus_paid, port_count, stage_factor) + correct = repeated_margin(2, 2, helper_minus_paid, port_count, stage_factor) + need(fault > 0 > correct, "doubled main credit hides the loss") + return { + "helper_minus_paid_at_t1": helper_minus_paid, + "evaluation_step": {"slope": step_slope, "constant": step_constant}, + "two_evaluation_margin": {"slope": margin_slope, "constant": margin_constant}, + "p2_k2_margin": correct, + "p2_k2_doubled_main": fault, + "separator": str(SEPARATOR[name]), + "jensen_base_floor": str(floor_base), + } + + +def main(): + invoices = local_invoices() + need(invoices["complex"]["helpers"] == {4: 28, 7: 7, 8: 47, 9: 326}, "complex helpers") + need(invoices["complex"]["paid"] == {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}, + "complex paid") + need(invoices["BIT"]["helpers"] == {8: 439}, "BIT helpers") + need(invoices["BIT"]["paid"] == {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, + "BIT paid") + report = {name: lane_report(name, invoice) for name, invoice in invoices.items()} + need(report["complex"]["helper_minus_paid_at_t1"] == -1856, "complex h(1)") + need(report["BIT"]["helper_minus_paid_at_t1"] == -1617, "BIT h(1)") + need(report["complex"]["two_evaluation_margin"] == {"slope": -1920, "constant": -3616}, + "complex K=2 form") + need(report["BIT"]["two_evaluation_margin"] == {"slope": -1680, "constant": -3138}, + "BIT K=2 form") + need(report["complex"]["p2_k2_margin"] == -7456, "complex p=2 witness") + need(report["BIT"]["p2_k2_margin"] == -6498, "BIT p=2 witness") + need(report["complex"]["p2_k2_doubled_main"] == 160, "complex ownership fault") + need(report["BIT"]["p2_k2_doubled_main"] == 162, "BIT ownership fault") + synthetic = separated_implication_fails_without_hypothesis() + rejected = controls(invoices) + need(rejected == [ + "extra_rank9_changes_complex_mass", + "positive_term_below_separator", + "indivisible_bit_target", + ], "failure controls") + print(json.dumps({ + "status": "PASS_REPEATED_CONTROLLER_RANK_MARGINS", + "lanes": report, + "synthetic_implication_failure": synthetic, + "rejected_controls": rejected, + "kappa_claimed": False, + "calculus_derivative_formalized": False, + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()