Certify repeated whole-controller rank-mass losses

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."
+}

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}