Derive the ordinary BIT admission constants and the controller surplus identity (no new κ)

research/admission-constant-derivation/README.md

@@ -0,0 +1,78 @@
+# admission-constant-derivation
+
+**No new κ.** Derives the ordinary BIT admission constants of
+`research/query-thinned-controllers` (reused unchanged by #4470,
+`research/joint-helper-lattice`) and the controller rank-surplus identity that
+`controller.py` checks as a hard-coded literal.
+
+## 1. atom, ordinary, admitted
+
+`query-thinned-controllers/verify.py` fixes C0 = 0.003459 (BIT uniform saving
+after tail strictification), C1 = 0.00345 (after delayed cover, with
+C0 − C1 > 256/2^26 for the prime rule), a_old = 0.0000384599 and
+
+    ordinary(δ) = (1 − δ)·C1 + δ·a_old,
+    admission:  ordinary(δ) < δ < 1 − ordinary(δ),
+
+where δ is the atom power (the linear adapter on width-e^δ atoms saves δ and
+must beat the ordinary saving; δ < 1 − ordinary keeps the stock sublinear).
+Since ordinary is decreasing in δ, the admissible atoms are exactly the open
+interval
+
+    ( C1/(1 + C1 − a_old), (1 − C1)/(1 − C1 + a_old) ) = (0.0034382702…, 0.9999614…).
+
+So **ordinary** is a formula, not a literal, and **atom** is a free parameter
+inside this interval: 0.004 is one admissible rounding (ordinary
+0.0034363538396), and the old 0.003 lies below the interval, which is the
+"old atom rejected" check. The supremum of the ordinary saving over all
+admissible atoms is the left endpoint 0.0034382702. **admitted** = 0.0034 is a
+rounding below it (relative loss 1.1%). Saturating the 2^26 prime allowance
+(C1 = C0 − 256/2^26) would raise the supremum only to 0.0034434.
+
+**κ effect: none.** #4470 needs only admitted > its complex tested saving
+0.003020155; the complex side binds. These constants matter only after the
+complex side exceeds about 0.0034, and then they are worth at most about +1.3%.
+
+## 2. The surplus identity `48*|thick| - 112` (complex) / `- 111` (BIT)
+
+With P ports of block width b, |thick| = p + 2 thick stages, per-stage helper
+target mass H and paid child mass C, the literal counting of
+`controller.inventories` gives, for every p and every prefix length a,
+
+    surplus = (p + 2)·(H − C + Σ_ports (2·b_port + 1)) − P.
+
+Proof: helpers and children contribute (p + 2)(H − C). Each prefix/suffix
+level j adds a main output of rank 1 + b(j + 1) and an idle call of rank
+b(j + 1), net +1 on each of 2 sides of a port, for p − 1 levels in total
+(independent of a). The full main output adds 2(1 + b(p + 2)) per port and the
+thin queries subtract 2p + 1 − (p + 2) = p − 1 per port. Summing,
+2b(p + 2) + 2 + 2(p − 1) − (p − 1) = (p + 2)(2b + 1) − 1 per port.
+
+Both sides have the same local balance s_loc = H − C + (2b + 1)P = 48:
+complex 3301 − 5157 + 17·112, BIT 3512 − 5129 + 15·111. The "48" is
+therefore this balance, not a property of width 8, and mixed widths only
+replace (2b + 1)P by the per-port sum. The verifier replays the literal
+counting for p = 2…40 and all a on both sides, matches both committed
+controller invoices (complex p = 17: 800, BIT p = 16: 753) and 200 random
+mixed-width instances.
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/admission-constant-derivation --check-only
+python3.12 scripts/research_package.py --package research/admission-constant-derivation
+```
+
+Runs in a few seconds with the standard library only.
+
+## Open next questions
+
+How far C0 and C1 can move toward the BIT root 0.00346 (see TASK.json). This
+is low priority while the complex side binds.
+
+## Credit
+
+Prepared by Mark (Matarener). The constants, controllers and invoices are from
+the query-thinned-controllers and joint-helper-lattice packages (#4440, #4470)
+and their sources. New work is Apache-2.0. Prepared with substantial Claude Code
+assistance.

research/admission-constant-derivation/RESULT.json

@@ -0,0 +1,43 @@
+{
+  "atom": {
+    "admitted": "17/5000",
+    "admitted_relative_loss": 0.011130656133333333,
+    "atom_interval_float": [
+      0.003438270203326716,
+      0.999961408443357
+    ],
+    "atom_interval_open": [
+      "1500000/436265887",
+      "9965500000/9965884599"
+    ],
+    "binding_side_margin": "75969/200000000",
+    "ordinary_at_atom": "8590884599/2500000000000",
+    "sup_ordinary": "1500000/436265887",
+    "sup_ordinary_at_C1_limit_float": 0.0034434200818683697,
+    "sup_ordinary_float": 0.003438270203326716
+  },
+  "kappa_effect": "none: complex tested 604031/200000000 binds; BIT admitted only needs to exceed it",
+  "schema": "admission-constant-derivation/1",
+  "status": "PASS_DERIVED_NO_NEW_KAPPA",
+  "surplus": {
+    "bit": {
+      "C": 5129,
+      "H": 3512,
+      "block": 7,
+      "committed_p": 16,
+      "committed_surplus": 753,
+      "ports": 111,
+      "s_loc": 48
+    },
+    "complex": {
+      "C": 5157,
+      "H": 3301,
+      "block": 8,
+      "committed_p": 17,
+      "committed_surplus": 800,
+      "ports": 112,
+      "s_loc": 48
+    },
+    "formula": "surplus = (p+2)*(H - C + sum_ports(2*b_port + 1)) - P"
+  }
+}

research/admission-constant-derivation/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/joint-helper-lattice/verify.py",
+      "usage": "input",
+      "git_blob": "0006dd15ca5597edfa506559124d2cdf3c493ae4",
+      "sha256": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f"
+    },
+    {
+      "path": "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json",
+      "usage": "input",
+      "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8",
+      "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6"
+    },
+    {
+      "path": "research/query-thinned-controllers/BIT-CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "89c400d5970024b3debe870c36ce43889beed001",
+      "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d"
+    },
+    {
+      "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9",
+      "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088"
+    },
+    {
+      "path": "research/query-thinned-controllers/controller.py",
+      "usage": "input",
+      "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583",
+      "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+    },
+    {
+      "path": "research/query-thinned-controllers/verify.py",
+      "usage": "input",
+      "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9",
+      "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950"
+    }
+  ]
+}

research/admission-constant-derivation/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "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.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "The ordinary BIT admission literals (atom 0.004, ordinary 0.0034363538396, admitted 0.0034) of research/query-thinned-controllers, reused unchanged by #4470 joint-helper-lattice, and the hard-coded rank-surplus check 48*|thick|-112/111 in its controller.py.",
+  "scope_change_reason": "#4633 and later discussion described these numbers as unexplained literals; any claim above the BIT ceiling 0.0034 needs them derived rather than copied.",
+  "bottleneck_link": "Side result: no new kappa. Removes an admission obstacle for any future complex-side gain beyond 0.0034 and shows the surplus identity is general in p, a and per-port widths.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the admissible atom interval, the supremum of the ordinary saving and the general surplus identity are derived and checked; do not re-run BIT tail strictification or change C0/C1.",
+  "outcome": "completed",
+  "evidence": "verify.py binds every literal from source, derives the exact atom interval and the closed-form surplus, replays the literal counting for p=2..40 and all a on both sides, matches both committed controller invoices, and checks 200 mixed-width instances; test_verify.py has six rejecting controls.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "How far can C0 and C1 (0.003459, 0.00345) be pushed toward the BIT root 0.00346?",
+      "why_it_matters": "They cap the ordinary saving at 0.0034383 (0.0034434 with the 2^26 prime rule saturated); this matters only once the complex side exceeds about 0.0034.",
+      "first_step": "Re-run the BIT tail strictification of query-thinned-controllers with a uniform saving closer to 0.00346 and record the first failing tail ratio.",
+      "blocked_by": "none; low priority while the complex side binds"
+    }
+  ]
+}

research/admission-constant-derivation/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/joint-helper-lattice/verify.py",
+    "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json",
+    "research/query-thinned-controllers/BIT-CONTROLLER.json",
+    "research/query-thinned-controllers/COMPLEX-CONTROLLER.json",
+    "research/query-thinned-controllers/controller.py",
+    "research/query-thinned-controllers/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Bind admission literals, BIT helper data and the surplus check from source; exact admissible atom interval and ordinary supremum; closed-form rank surplus against literal counting (p=2..40, all a, both sides), both committed controller invoices and 200 mixed-width instances; receipt replay."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Rejecting controls: atoms outside the interval, admitted above the supremum, dropped lost-helper term, changed helper count, one mixed-width port."
+    }
+  ]
+}

research/admission-constant-derivation/test_verify.py

@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Rejecting controls for verify.py."""
+import sys
+import unittest
+from fractions import Fraction as Q
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+import verify as v  # noqa: E402
+
+S = v.bind_sources()
+
+
+class Controls(unittest.TestCase):
+    def test_atom_at_or_below_left_endpoint_fails(self):
+        lo, _ = v.atom_interval(S['C1'], S['old'])
+        for d in (lo, lo-Q(1, 10**9), Q('.0034')):
+            self.assertFalse(v.admissible(S['C1'], S['old'], d))
+
+    def test_atom_at_or_above_right_endpoint_fails(self):
+        _, hi = v.atom_interval(S['C1'], S['old'])
+        self.assertFalse(v.admissible(S['C1'], S['old'], hi))
+        self.assertFalse(v.admissible(S['C1'], S['old'], Q(1)))
+
+    def test_admitted_above_sup_impossible(self):
+        lo, hi = v.atom_interval(S['C1'], S['old'])
+        target = lo+Q(1, 10**9)
+        for d in (lo+Q(1, 10**12), Q('.004'), (lo+hi)/2):
+            self.assertLess(v.ordinary(S['C1'], S['old'], d), target)
+
+    def test_dropping_lost_helper_term_fails(self):
+        helpers, children, ports, block = S['sides']['complex']
+        lit = v.literal_surplus(helpers, children, [block]*ports, 17, 5)[0]
+        H = sum(r*n for r, n in helpers.items()); C = sum(r*n for r, n in children.items())
+        self.assertNotEqual(lit, 19*(H-C+(2*block+1)*ports))
+
+    def test_width_only_reading_fails(self):
+        # 48 is the local balance, not a width-8 constant: change one helper count
+        helpers, children, ports, block = S['sides']['bit']
+        changed = dict(helpers); changed[8] += 1
+        lit = v.literal_surplus(changed, children, [block]*ports, 16, 3)[0]
+        self.assertNotEqual(lit, 48*18-ports)
+        self.assertEqual(lit, v.closed_surplus(changed, children, [block]*ports, 16))
+
+    def test_mixed_widths_break_uniform_formula(self):
+        helpers, children, ports, block = S['sides']['complex']
+        widths = [block]*(ports-1)+[7]
+        lit = v.literal_surplus(helpers, children, widths, 16, 4)[0]
+        self.assertNotEqual(lit, 48*18-ports)
+        self.assertEqual(lit, v.closed_surplus(helpers, children, widths, 16))
+
+
+if __name__ == '__main__':
+    unittest.main(verbosity=2)