diff --git a/research/admission-constant-derivation/README.md b/research/admission-constant-derivation/README.md new file mode 100644 index 0000000000..7cf0f44634 --- /dev/null +++ b/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. diff --git a/research/admission-constant-derivation/RESULT.json b/research/admission-constant-derivation/RESULT.json new file mode 100644 index 0000000000..ef18602d41 --- /dev/null +++ b/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" + } +} diff --git a/research/admission-constant-derivation/SOURCES.json b/research/admission-constant-derivation/SOURCES.json new file mode 100644 index 0000000000..3ceadcf79b --- /dev/null +++ b/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" + } + ] +} diff --git a/research/admission-constant-derivation/TASK.json b/research/admission-constant-derivation/TASK.json new file mode 100644 index 0000000000..55d87de66a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/admission-constant-derivation/VERIFY.json b/research/admission-constant-derivation/VERIFY.json new file mode 100644 index 0000000000..ce169ac1e7 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/admission-constant-derivation/test_verify.py b/research/admission-constant-derivation/test_verify.py new file mode 100644 index 0000000000..a3387f385b --- /dev/null +++ b/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) diff --git a/research/admission-constant-derivation/verify.py b/research/admission-constant-derivation/verify.py new file mode 100644 index 0000000000..10163abba8 --- /dev/null +++ b/research/admission-constant-derivation/verify.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Derive the ordinary BIT admission constants and the controller rank-surplus +identity used by research/query-thinned-controllers and inherited by #4470. + +1. atom/ordinary/admitted: the literals are bound from source; the admissible + atom set is an exact open interval, 0.004 lies in it, 0.003 does not, and the + supremum of the ordinary saving is its left endpoint. +2. controller.py's check surplus == 48*|thick| - 112 (complex) / - 111 (BIT) + is the case s_loc = 48 of surplus = (p+2)*(H - C + sum_ports(2 b + 1)) - P, + for every p and prefix length a, and for per-port block widths. + +Exact rationals only; runs in a few seconds. No new kappa. +Mark (Matarener), with substantial Claude Code assistance. Apache-2.0. +""" +import ast +import json +import random +import re +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +QTC = ROOT/'research/query-thinned-controllers' +JHL = ROOT/'research/joint-helper-lattice/verify.py' +THREE = ROOT/'research/kappa-rebuild/complex/full-identity-certificates/RESULT.json' + + +def need(ok, label): + if not ok: + raise SystemExit('FAIL: '+label) + print('PASS', label) + + +# ------------------------------------------------------------ source binding +def bind_sources(): + text = (QTC/'verify.py').read_text(encoding='utf-8') + m = re.search(r"before, after, atom, old = Q\('([.\d]+)'\), Q\('([.\d]+)'\), Q\('([.\d]+)'\), Q\('([.\d]+)'\)", text) + need(m is not None, 'Bind before/after/atom/old literals in query-thinned verify.py') + C0, C1, atom, old = (Q(x) for x in m.groups()) + m = re.search(r"ordinary, admitted = \(1-atom\)\*after\+atom\*old, Q\('([.\d]+)'\)", text) + need(m is not None, 'Bind ordinary formula and admitted literal') + admitted = Q(m.group(1)) + need('atom > ordinary > admitted and atom < 1-ordinary' in text and "2**26 > 256/(before-after)" in text, + 'Bind admission predicates and prime allowance') + jhl = JHL.read_text(encoding='utf-8') + m = re.search(r"KAPPA, TESTED = Q\('([.\d]+)'\), Q\('([.\d]+)'\)", jhl) + need(m is not None and "atom==Q('.004')" in jhl and "atom>ordinary>admitted>TESTED" in jhl, + 'Bind #4470 reuse: atom 0.004 and admitted > TESTED') + kappa, tested = (Q(x) for x in m.groups()) + ctrl = (QTC/'controller.py').read_text(encoding='utf-8') + tree = ast.parse(ctrl) + bit = {} + for node in ast.walk(tree): + if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name) \ + and node.targets[0].id in ('helpers', 'children') and isinstance(node.value, ast.Dict): + bit[node.targets[0].id] = ast.literal_eval(node.value) + need(set(bit) == {'helpers', 'children'}, 'Bind BIT helper/child literals in controller.py') + need("48*len(thick)-112 if kind == 'complex' else 48*len(thick)-111" in ctrl, 'Bind the hard-coded surplus check') + three = json.loads(THREE.read_text(encoding='utf-8'))['providers']['THREE-base'] + cx = ({int(k): v for k, v in three['helper_boundary']['widths'].items()}, + {int(k): v for k, v in three['unsplit_replays']['forward']['paid_profile'].items()}) + return dict(C0=C0, C1=C1, atom=atom, old=old, admitted=admitted, kappa=kappa, tested=tested, + sides={'complex': (cx[0], cx[1], 112, 8), 'bit': (bit['helpers'], bit['children'], 111, 7)}) + + +# ------------------------------------------------------------ part 1: atom +def ordinary(C1, old, d): + return (1-d)*C1+d*old + + +def admissible(C1, old, d): + o = ordinary(C1, old, d) + return o < d < 1-o + + +def atom_interval(C1, old): + """ordinary decreases in d, so o(d) < d iff d > lo and d < 1-o(d) iff d < hi.""" + return C1/(1+C1-old), (1-C1)/(1-C1+old) + + +def part_atom(s): + C0, C1, old, atom, admitted = s['C0'], s['C1'], s['old'], s['atom'], s['admitted'] + lo, hi = atom_interval(C1, old) + need(ordinary(C1, old, lo) == lo and 1-ordinary(C1, old, hi) == hi, 'Interval endpoints are the two fixed points') + eps = Q(1, 10**12) + need(all(admissible(C1, old, d) for d in (lo+eps, (lo+hi)/2, hi-eps)) and + not any(admissible(C1, old, d) for d in (lo, hi, lo-eps, hi+eps)), 'Admissible atoms = open interval (lo, hi)') + need(lo < atom < hi and ordinary(C1, old, atom) == Q('0.0034363538396'), 'Atom 0.004 admissible; ordinary 0.0034363538396') + need(not admissible(C1, old, Q('.003')), 'Old atom 0.003 rejected') + need(admitted < ordinary(C1, old, atom) and admitted > s['tested'], 'admitted 0.0034 < ordinary and > #4470 tested 0.003020155') + need(C0-C1 > Q(256, 2**26), 'Delayed-cover gap exceeds 256/2^26') + c1max = C0-Q(256, 2**26) + return {'atom_interval_open': [str(lo), str(hi)], 'atom_interval_float': [float(lo), float(hi)], + 'ordinary_at_atom': str(ordinary(C1, old, atom)), 'sup_ordinary': str(lo), 'sup_ordinary_float': float(lo), + 'admitted': str(admitted), 'admitted_relative_loss': float(1-admitted/lo), + 'sup_ordinary_at_C1_limit_float': float(c1max/(1+c1max-old)), + 'binding_side_margin': str(admitted-s['tested'])} + + +# ------------------------------------------------------------ part 2: surplus +def literal_surplus(helpers, children, widths, p, a): + """Same counting as controller.inventories, with one block width per port.""" + thick = {0, 2*p, *range(1, 2*p, 2)} + targets = Counter({r: len(thick)*n for r, n in helpers.items()}) + paid = Counter({r: len(thick)*n for r, n in children.items()}) + paid[1] += len(widths)*(2*p+1-len(thick)) + for b in widths: + targets[1+b*(p+2)] += 2 + for length in (a, p-1-a): + for j in range(1, length+1): + targets[1+b*(j+1)] += 2 + paid[b*(j+1)] += 2 + return sum(r*n for r, n in targets.items())-sum(r*n for r, n in paid.items()), targets, paid + + +def closed_surplus(helpers, children, widths, p): + H = sum(r*n for r, n in helpers.items()); C = sum(r*n for r, n in children.items()) + return (p+2)*(H-C+sum(2*b+1 for b in widths))-len(widths) + + +def part_surplus(s): + out = {} + for kind, (helpers, children, ports, block) in s['sides'].items(): + H = sum(r*n for r, n in helpers.items()); C = sum(r*n for r, n in children.items()) + s_loc = H-C+(2*block+1)*ports + need(s_loc == 48, '%s: s_loc = H - C + (2b+1)P = %d - %d + %d = 48' % (kind, H, C, (2*block+1)*ports)) + widths = [block]*ports + for p in range(2, 41): + for a in range(p): + lit = literal_surplus(helpers, children, widths, p, a)[0] + if lit != closed_surplus(helpers, children, widths, p) or lit != 48*(p+2)-ports: + need(False, '%s literal count p=%d a=%d' % (kind, p, a)) + need(True, '%s: literal counting = closed form = 48(p+2) - %d for p = 2..40, every a' % (kind, ports)) + ctrl = json.loads((QTC/('%s-CONTROLLER.json' % kind.upper())).read_text(encoding='utf-8'))['invoice'] + T = ctrl['thick_calls']; p = T-2 + mass = lambda d: sum(int(r)*n for r, n in d.items()) + need(mass(ctrl['targets'])-mass(ctrl['paid']) == ctrl['rank_surplus'] == closed_surplus(helpers, children, widths, p), + '%s: committed p=%d invoice surplus %d matches the closed form' % (kind, p, ctrl['rank_surplus'])) + out[kind] = {'H': H, 'C': C, 'ports': ports, 'block': block, 's_loc': s_loc, 'committed_p': p, + 'committed_surplus': ctrl['rank_surplus']} + rng = random.Random(4470) + helpers, children = s['sides']['complex'][:2] + for _ in range(200): + widths = [rng.randint(1, 12) for _ in range(rng.randint(1, 20))] + p = rng.randint(2, 30); a = rng.randrange(p) + if literal_surplus(helpers, children, widths, p, a)[0] != closed_surplus(helpers, children, widths, p): + need(False, 'mixed widths %s p=%d a=%d' % (widths, p, a)) + need(True, 'Mixed per-port widths: 200 random instances match (p+2)(H - C + sum(2b+1)) - P') + out['formula'] = 'surplus = (p+2)*(H - C + sum_ports(2*b_port + 1)) - P' + return out + + +def run(): + s = bind_sources() + return {'schema': 'admission-constant-derivation/1', 'status': 'PASS_DERIVED_NO_NEW_KAPPA', + 'atom': part_atom(s), 'surplus': part_surplus(s), + 'kappa_effect': 'none: complex tested %s binds; BIT admitted only needs to exceed it' % s['tested']} + + +if __name__ == '__main__': + result = run() + out = HERE/'RESULT.json' + if '--write' in sys.argv: + out.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n', encoding='utf-8', newline='\n') + else: + need(result == json.loads(out.read_text(encoding='utf-8')), 'Receipt matches exact replay') + print(json.dumps({k: result[k] for k in ('status', 'kappa_effect')}))