From 324d14bce8cfc7cda174e089029be06c2bcea9dd Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 03:53:28 +0000 Subject: [PATCH] Record that the selected k8 word emits no paid child above rank 8. Every legal F2^9 frame assignment has graph climbs of rank at most 5 and eight fixed rank-8 centre descents, so the rank-44 local-child threshold is outside this alphabet. Co-authored-by: unpaidmoon --- .../selected-k8-child-rank-bound/README.md | 115 ++++ .../selected-k8-child-rank-bound/RESULT.json | 42 ++ .../selected-k8-child-rank-bound/SOURCES.json | 24 + .../selected-k8-child-rank-bound/TASK.json | 78 +++ .../selected-k8-child-rank-bound/VERIFY.json | 21 + .../selected-k8-child-rank-bound/verify.py | 508 ++++++++++++++++++ 6 files changed, 788 insertions(+) create mode 100644 research/selected-k8-child-rank-bound/README.md create mode 100644 research/selected-k8-child-rank-bound/RESULT.json create mode 100644 research/selected-k8-child-rank-bound/SOURCES.json create mode 100644 research/selected-k8-child-rank-bound/TASK.json create mode 100644 research/selected-k8-child-rank-bound/VERIFY.json create mode 100644 research/selected-k8-child-rank-bound/verify.py diff --git a/research/selected-k8-child-rank-bound/README.md b/research/selected-k8-child-rank-bound/README.md new file mode 100644 index 0000000000..5a40836bd4 --- /dev/null +++ b/research/selected-k8-child-rank-bound/README.md @@ -0,0 +1,115 @@ +# Largest paid child rank of the selected k8 word + +**Scoped rank bound. No new κ.** The selected conditional result stays +`0.001672660197076918`. + +The rank-cap handoff on the selected complex local word asks for the largest +child rank a physical word on that template can emit, counting frame climbs +and the cone restrictions that restoration imposes. On the selected k8 word, +content hash `c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8`, +the answer is **8**. + +## Contract + +Frames are subspaces of `F2^9`. A legal assignment may change the frame of any +A, B or early-cleanup gate inside its forward/backward interval. Frames stay +nested along each register. Centre and target pins, start and end frames, and +the low-end cone ceilings stay fixed. This is the frame contract of the +selected word's native auditor, enlarged only by charging a climb into a pin +instead of requiring that climb to be zero. + +A paid child is one of two things: + +- a strict climb of dimension `d = dim(F') - dim(F)` on one register edge; +- one of the eight centre descents, read off the fixed centre frames and the + cut. + +Each register pays its own climb. Idle packing at rank up to 51 is not a child +of this word. + +## Result + +Every legal assignment obeys the following, recomputed from the pinned word: + +| Fact | Value | +|---|---| +| Largest graph climb | **5** | +| Centre descents | eight children, each of rank **8** | +| Largest paid child rank | **8**, attained by those descents | +| Rank 44 emitted | no | +| Free / forced gates | 1,741 / 3,672 | +| Interval sizes | 1,098 gates with 2 frames, 613 with 5, 30 with 16 | +| Edges whose interval allows a jump above the recorded jump | 3,222 (multiplicity) | +| Same climb cap with cone ceilings removed | still 5 | + +The 82 register-edges that can jump by 5 are exactly the support of rank 5. +Their interval minima are 5 (32 edges), 4 (26) and 3 (24). The recorded word +uses jump 5 on all 82, so rank 5 is attained and no legal assignment adds +another rank-5 climb. Fifty of those edges can drop. Other edges can rise +only as far as 4. No edge interval contains a jump of 6 or more. Reassignment +can move mass among ranks 1 through 5. It cannot create a paid child of rank +9, 16, 44 or 51. + +A second walk, charging the recorded sections the way the native auditor does, +reproduces the published profile `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`. +The two routes share no climb loop. The free-gate and interval counts match +the census already published for this word's moment bound. + +The ambient lemma is separate and weaker: any nested pair of subspaces of +`F2^9` jumps by at most 9. The edge intervals give 5. A vector with bit 9 set +is rejected. A claimed cap of 4 is rejected because 82 edges allow 5. + +## What this does not say + +This is the native climb alphabet of one fixed scalar word. It does not price +a different child identity that bundles several rank-1 climbs into one block +child, and it does not rerun the moment duals. A block whose rank is the +number of gathered payloads would be a changed tariff. The recorded word has +no single-gate incoming climb mass above 8, but that observation is not a +census of multi-gate co-frame groups. Changed gates, entrances or end frames +can leave this interval data. + +No supplier, invoice, native admission or selected-frontier change is claimed. + +## Reproduce + +Python 3.12, standard library only, from the repository root. About two +seconds. + +```sh +python3.12 -I -B research/selected-k8-child-rank-bound/verify.py +python3.12 -B scripts/research_package.py --package research/selected-k8-child-rank-bound +``` + +Expected final line: + +```text +PASS_SELECTED_K8_CHILD_RANK_BOUND max_paid_rank=8 max_climb=5 centre=8x8 rank44=0 free_gates=1741 increasable_edges=3222 no_new_kappa +``` + +`verify.py --write` regenerates `RESULT.json`. Without `--write` the checker +requires that receipt byte for byte. + +## Open next questions + +- **Can one co-frame block on this same word have rank above 8?** The native + alphabet charges each climb separately, so a block child is a different + identity. The frames needed for that census are the intervals built here. + Owned temporary lifetimes are still not in the word archive, which is the + remaining blocker named by the co-frame gate screen. +- **Does one legal scalar edit open a register edge of jump 6 or more?** The + cap of 5 is a property of this gate list and these pins. A rewrite has to + change an interval before the rank bound moves. + +## Credit + +The word, the `F2^9` frame contract and the published interval census are the +selected k8 frame-ceiling package (PR #1671, Gareth Davidson, using navinor's +frame method and the gauge44 auditor). The rank-44 threshold this bound is +compared with is the open question in Discussion #1166 comment 19021222, +recorded from PR #3701. The separate block-reblocking tariff is PR #3039, +PR #3066 and `research/rank-shape-coframe-bill-seed850bc3`. This package does +not import those programs. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent +human or formal-kernel review is claimed. Apache-2.0. diff --git a/research/selected-k8-child-rank-bound/RESULT.json b/research/selected-k8-child-rank-bound/RESULT.json new file mode 100644 index 0000000000..5b14635ae0 --- /dev/null +++ b/research/selected-k8-child-rank-bound/RESULT.json @@ -0,0 +1,42 @@ +{ + "ambient_dimension": 9, + "centre_descent_count": 8, + "centre_descent_rank": 8, + "edge_max_histogram": { + "0": 5529, + "1": 2712, + "2": 1790, + "3": 738, + "4": 254, + "5": 82 + }, + "edges_whose_jump_can_increase": 3222, + "forced_gates": 3672, + "free_gates": 1741, + "given_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "interval_sizes": { + "2": 1098, + "5": 613, + "16": 30 + }, + "largest_graph_climb": 5, + "largest_paid_child_rank": 8, + "max_climb_without_cone_ceilings": 5, + "no_new_kappa": true, + "rank5_capable_edges_by_minimum": { + "3": 24, + "4": 26, + "5": 32 + }, + "rank_44_emitted": false, + "schema": "selected-k8-child-rank-bound-v1", + "section_walk_agrees": true, + "word_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8" +} diff --git a/research/selected-k8-child-rank-bound/SOURCES.json b/research/selected-k8-child-rank-bound/SOURCES.json new file mode 100644 index 0000000000..b5ae238167 --- /dev/null +++ b/research/selected-k8-child-rank-bound/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz", + "usage": "input", + "git_blob": "723decbca8995e916d6f4b783aa3e1ddd4eb47fe", + "sha256": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289" + } + ] +} diff --git a/research/selected-k8-child-rank-bound/TASK.json b/research/selected-k8-child-rank-bound/TASK.json new file mode 100644 index 0000000000..eafa1d6831 --- /dev/null +++ b/research/selected-k8-child-rank-bound/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "refined", + "actual_scope": "On the selected k8 word, what is the largest paid child rank any legal monotone F2^9 frame assignment can emit?", + "scope_change_reason": "The card's second method asks for the best effective child rank on one fixed support alphabet, with copies, frames and restoration counted. This package answers that bound for the selected k8 native frame alphabet. It does not synthesize a block decoder or a profile aimed at the +5% gate.", + "bottleneck_link": "Rank-1 children are about half of recursive cost. The rank-cap handoff says a target-scale local saving on this template needs a paid child of rank at least 44. This word's frame alphabet never emits a paid child above rank 8, so that histogram is not a child of the selected word.", + "budget_minutes": 60, + "stop_rule": "Stop once the edge-interval census and the independent section walk agree on the published profile and on a climb cap of 5. Do not search a different scalar word or a block-bundling identity.", + "outcome": "completed", + "evidence": "RESULT.json: largest paid child rank 8, attained by eight fixed centre descents; every register-edge interval has dimension jump at most 5 (82 edges can reach 5; their minima are 5, 4 and 3 on 32, 26 and 24 edges); 1741 free and 3672 forced gates with interval sizes 2/5/16 matching the published census; cone ceilings do not change the cap; section walk reproduces the published profile; rank 44 does not occur.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance. No independent human or formal-kernel review claimed. The checker does not import the predecessor frame model.", + "open_questions": [ + { + "question": "Can one co-frame block on this same scalar word have rank above 8?", + "why_it_matters": "The native alphabet charges each climb separately. A block child that replaces several rank-1 climbs by one higher-rank child is a different tariff, and it is the identity the rank-cap handoff would need in order to emit rank 44.", + "first_step": "Partition the 2412 recorded rank-1 climbs into co-frame groups using the intervals this census builds, then price one group with the existing per-block restoration tax.", + "blocked_by": "Owned temporary lifetimes are still not recorded in the word archive." + }, + { + "question": "Does one legal scalar edit open a register edge whose interval jump exceeds 5?", + "why_it_matters": "The climb cap is a property of this fixed gate list, pins and end frames. A different word can leave the interval data.", + "first_step": "Name one legal rewrite that changes an active frame interval and recompute the edge-maximum census on that word.", + "blocked_by": "No such rewrite is proposed in this package." + } + ] +} diff --git a/research/selected-k8-child-rank-bound/VERIFY.json b/research/selected-k8-child-rank-bound/VERIFY.json new file mode 100644 index 0000000000..87856a296f --- /dev/null +++ b/research/selected-k8-child-rank-bound/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Selected-word hash, edge-interval climb cap 5, eight rank-8 centre descents, largest paid rank 8, free-gate tie-out 1741, rank-5 minima, cone-ceiling sensitivity, section-walk profile, outside-vector and false-cap-4 controls, RESULT.json byte match." + } + ] +} diff --git a/research/selected-k8-child-rank-bound/verify.py b/research/selected-k8-child-rank-bound/verify.py new file mode 100644 index 0000000000..04745ae9d1 --- /dev/null +++ b/research/selected-k8-child-rank-bound/verify.py @@ -0,0 +1,508 @@ +#!/usr/bin/env python3 +"""Largest paid child rank of the selected k8 word under its frame contract. + +A paid child is one strict dimension jump of nested frames along a register, +or one fixed centre descent. Frames are subspaces of F2^9. This checker +rebuilds the event graph, the forward/backward frame intervals and the +low-end cone ceilings, then enumerates every nested pair on every edge. +It does not import the predecessor frame model. +""" + +import gzip +import hashlib +import json +import sys +from collections import Counter, defaultdict +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +WORD = ROOT / "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz" +RECEIPT = Path(__file__).resolve().parent / "RESULT.json" +WORD_SHA = "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8" +PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +H = 9 +FULL = tuple(1 << i for i in range(H - 1, -1, -1)) +TARGET_RANK = 44 + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def eliminate(vs): + piv = {} + for a in vs: + need(a >= 0, "negative frame vector") + while a: + bit = a.bit_length() - 1 + if bit in piv: + a ^= piv[bit] + else: + piv[bit] = a + break + for k in sorted(piv): + for j in piv: + if j > k and (piv[j] >> k) & 1: + piv[j] ^= piv[k] + return tuple(piv[k] for k in sorted(piv, reverse=True)) + + +def basis(vs): + out = eliminate(vs) + need(all(a < (1 << H) for a in out), "frame vector outside F2^9") + return out + + +def contained(a, b): + return basis(list(a) + list(b)) == tuple(b) + + +def join(frames): + return basis(x for f in frames for x in f) + + +def meet(a, b): + rows = [(u << H) | u for u in a] + [x << H for x in b] + return basis(r for r in eliminate(rows) if r >> H == 0) + + +def interval(lo, hi): + need(contained(lo, hi), "empty frame interval") + comp, cur = [], list(lo) + for x in hi: + if len(basis(cur + [x])) > len(basis(cur)): + comp.append(x) + cur.append(x) + k = len(comp) + need(k <= 4, "quotient dimension above 4") + vectors = list(range(1, 1 << k)) + out = [] + for mask in range(1 << len(vectors)): + chosen = {vectors[i] for i in range(len(vectors)) if (mask >> i) & 1} + if all((p ^ q) in chosen for p in chosen for q in chosen if p != q): + lifted = [] + for a in chosen: + x = 0 + for i in range(k): + if (a >> i) & 1: + x ^= comp[i] + lifted.append(x) + out.append(basis(list(lo) + lifted)) + need(len(set(out)) == len(out), "duplicate interval frame") + return out + + +def registers(e): + return (e[1], e[2]) if e[0] == "add" else (e[1],) + + +def apply(e, rows, dual=False): + if e[0] == "add": + t, s = e[1], e[2] + q = Fraction(e[3], e[4]) + if dual: + t, s, q = s, t, -q + dst = rows[t] + for k, x in list(rows[s].items()): + a = dst.get(k, Fraction(0)) + q * x + if a: + dst[k] = a + else: + dst.pop(k, None) + elif e[0] == "scale": + t = e[1] + q = Fraction(e[2], e[3]) + if dual: + q = 1 / q + rows[t] = {k: q * x for k, x in rows[t].items()} + else: + raise ValueError("unknown scalar primitive") + + +def invert(e): + r = list(e) + if r[0] == "add": + r[3] = -r[3] + else: + r[2], r[3] = r[3], r[2] + return r + + +def cone_ceilings(w, n, v, low_ends): + ident = lambda: [{k: Fraction(1)} for k in range(n)] + main = w["A"] + w["cut"] + w["B"] + raw = ident() + for e in main: + apply(e, raw) + dirt = [{} for _ in range(n)] + for y in range(v, 2 * v): + dirt[y] = {k: a for k, a in raw[y].items() if k >= 2 * v} + for e in w["precondition"]: + apply(e, dirt) + compensation = [ + ["add", y, k, -a.numerator, a.denominator, []] + for y in range(v, 2 * v) + for k, a in sorted(dirt[y].items()) + ] + prefix = w["precondition"] + compensation + main + p, pinv = ident(), ident() + for e in prefix: + apply(e, p) + for e in reversed(prefix): + apply(invert(e), pinv) + holders = defaultdict(set) + for k in range(n): + for j in p[k]: + holders[j].add(k) + ceil = {} + for q, U in low_ends.items(): + for k in set(pinv[q]) | holders[q]: + if k != q: + ceil[k] = meet(ceil.get(k, FULL), U) + return ceil + + +def load_word(): + blob = WORD.read_bytes() + raw = gzip.decompress(blob) + need(hashlib.sha256(raw).hexdigest() == WORD_SHA, "selected word content hash") + w = json.loads(raw) + rep = w["report"] + profile = {int(r): n for r, n in rep["local_profile"].items()} + need(profile == PROFILE, "published local profile") + need(rep["h"] == H and rep["v"] == 112 and rep["R"] == 480, "word dimensions") + need(sum(r * n for r, n in profile.items()) == 5586, "local rank mass") + return w + + +def build(w, use_cones=True): + rep = w["report"] + v, R = rep["v"], rep["R"] + n = 2 * v + R + end = [FULL] * v + [ + basis(x for x in range(1, 1 << H) if (x & p).bit_count() % 2 == 0) + for p in w["ports"] + ] + [FULL] * R + low = {int(q): basis(U) for q, U in w.get("helper_final", {}).items()} + for q, U in low.items(): + need(2 * v <= q < n, "helper final register") + end[q] = U + start = [(p,) for p in w["ports"]] + [()] * (v + R) + for q, U in w.get("start_extra", {}).items(): + need(2 * v <= int(q) < n, "non-helper entrance") + start[int(q)] = basis(U) + early = w.get("early_cleanup", []) + need(len({i for i, _ in early}) == len(early), "duplicate early cleanup") + tail = [w["cleanup"][i][:-1] + [U] for i, U in early] + lev = {int(t): basis(U) for t, U in w.get("target_levels", {}).items()} + pins = {q: basis(U) for q, U in zip(w["centers"], w["center_frames"])} + need(len(pins) == 8, "eight centres") + for t in range(v): + need(v + t not in pins, "target pin collision") + pins[v + t] = lev.get(t, ()) + centre = [] + for q, U in zip(w["centers"], w["center_frames"]): + U = basis(U) + served = {lev.get(e[1] - v, ()) for e in w["cut"] if e[2] == q} + for T in sorted(served, key=lambda x: -len(x)): + need(contained(T, U), "centre path not nested") + if T != U: + centre.append(len(U) - len(T)) + U = T + gates = [("A", e) for e in w["A"]] + [("B", e) for e in w["B"]] + [ + ("T", e) for e in tail + ] + given = [basis(e[-1]) for _, e in gates] + regs = [registers(e) for _, e in gates] + nA, nB = len(w["A"]), len(w["B"]) + need((nA, nB, len(tail)) == (3451, 1846, 116), "section sizes") + fixed = {} + for q in range(n): + fixed[("S", q)] = start[q] + fixed[("E", q)] = end[q] + for q, U in pins.items(): + fixed[("P", q)] = U + chains = defaultdict(list) + for q in range(n): + chains[q].append(("S", q)) + boundary = {} + for i, rs in enumerate(regs): + if i == nA: + for q in pins: + chains[q].append(("P", q)) + if i == nA + nB: + for q in range(n): + boundary[q] = len(chains[q]) - 1 + for q in rs: + chains[q].append(("G", i)) + for q in range(n): + chains[q].append(("E", q)) + order = [("S", q) for q in range(n)] + for i in range(len(gates)): + if i == nA: + order += [("P", q) for q in pins] + order.append(("G", i)) + order += [("E", q) for q in range(n)] + position = {node: k for k, node in enumerate(order)} + pred, succ = defaultdict(list), defaultdict(list) + edges = Counter() + for q, ch in chains.items(): + for a, b in zip(ch, ch[1:]): + need(position[a] < position[b], "chain order") + succ[a].append(b) + pred[b].append(a) + edges[(a, b)] += 1 + lo, hi = {}, {} + for node in order: + if node in fixed: + lo[node] = fixed[node] + for a in pred[node]: + need(contained(lo[a], fixed[node]), "fixed frame below its join") + else: + lo[node] = join(lo[a] for a in pred[node]) + ceil = cone_ceilings(w, n, v, low) if use_cones else {} + ceil_at = defaultdict(list) + for q, k in boundary.items(): + if q in ceil: + ceil_at[chains[q][k]].append(ceil[q]) + for node in reversed(order): + if node in fixed: + hi[node] = fixed[node] + else: + U = FULL + for b in succ[node]: + U = meet(U, hi[b]) + for C in ceil_at[node]: + U = meet(U, C) + hi[node] = U + need(contained(lo[node], hi[node]), "empty domain") + domain = {} + for i in range(len(gates)): + node = ("G", i) + if lo[node] != hi[node]: + domain[node] = interval(lo[node], hi[node]) + need(given[i] in domain[node], "given frame outside its interval") + else: + need(given[i] == lo[node], "given frame differs from the forced frame") + return { + "edges": dict(edges), + "domain": domain, + "lo": lo, + "hi": hi, + "given": given, + "centre": centre, + "fixed": fixed, + } + + +def frames_of(graph, node): + if node in graph["domain"]: + return graph["domain"][node] + if node in graph["fixed"]: + return [graph["fixed"][node]] + return [graph["lo"][node]] + + +def edge_bounds(graph): + """Maximum dimension jump of each edge over its complete frame intervals.""" + bounds = {} + given = {} + for (a, b), m in graph["edges"].items(): + best = 0 + least = H + nested = False + for Fa in frames_of(graph, a): + for Fb in frames_of(graph, b): + if contained(Fa, Fb): + d = len(Fb) - len(Fa) + best = max(best, d) + least = min(least, d) + nested = True + need(nested, "edge has no monotone frame pair") + # The given assignment uses the recorded gate frame, else the fixed frame. + if a[0] == "G" and a in graph["domain"]: + Fa = graph["given"][a[1]] + else: + Fa = frames_of(graph, a)[0] + if b[0] == "G" and b in graph["domain"]: + Fb = graph["given"][b[1]] + else: + Fb = frames_of(graph, b)[0] + need(contained(Fa, Fb), "given assignment is not monotone") + d = len(Fb) - len(Fa) + bounds[(a, b)] = (least, best, m) + given[(a, b)] = d + need(least <= d <= best, "given jump outside the interval") + return bounds, given + + +def given_profile(graph, given): + count = Counter() + for (a, b), d in given.items(): + if d: + count[d] += graph["edges"][(a, b)] + for d in graph["centre"]: + count[d] += 1 + return dict(sorted(count.items())) + + +def section_profile(w): + """Second route: walk the recorded sections, as the native auditor charges them.""" + rep = w["report"] + v, R = rep["v"], rep["R"] + n = 2 * v + R + end = [FULL] * v + [ + basis(x for x in range(1, 1 << H) if (x & p).bit_count() % 2 == 0) + for p in w["ports"] + ] + [FULL] * R + for q, U in w.get("helper_final", {}).items(): + end[int(q)] = basis(U) + start = [(p,) for p in w["ports"]] + [()] * (v + R) + for q, U in w.get("start_extra", {}).items(): + start[int(q)] = basis(U) + early = {i: U for i, U in w.get("early_cleanup", [])} + tail = [w["cleanup"][i][:-1] + [U] for i, U in early.items()] + lev = {int(t): basis(U) for t, U in w.get("target_levels", {}).items()} + cur = list(start) + paid = Counter() + + def climb(q, U): + U = basis(U) + need(contained(cur[q], U), "section walk left the monotone contract") + d = len(U) - len(cur[q]) + if d: + paid[d] += 1 + cur[q] = U + + for section in ("A", "B"): + if section == "B": + for t in range(v): + need(cur[v + t] == lev.get(t, ()), "target level mismatch") + for q, U0 in zip(w["centers"], w["center_frames"]): + U = basis(U0) + need(cur[q] == U, "centre entrance mismatch") + served = {lev.get(e[1] - v, ()) for e in w["cut"] if e[2] == q} + for T in sorted(served, key=lambda x: -len(x)): + need(contained(T, U), "centre descent not nested") + if T != U: + paid[len(U) - len(T)] += 1 + U = T + for e in w[section]: + for q in registers(e): + climb(q, e[-1]) + for e in tail: + for q in registers(e): + climb(q, e[-1]) + for q, U in enumerate(end): + climb(q, U) + return dict(sorted(paid.items())) + + +def census(w, use_cones=True): + graph = build(w, use_cones=use_cones) + bounds, given = edge_bounds(graph) + max_jump = max(best for _, best, _ in bounds.values()) + hist = Counter() + increases = 0 + rank5_min = Counter() + for (a, b), (least, best, m) in bounds.items(): + hist[best] += m + if given[(a, b)] < best: + increases += m + if best == 5: + rank5_min[least] += m + sizes = Counter(len(fs) for fs in graph["domain"].values()) + quotients = Counter() + for node, fs in graph["domain"].items(): + # Interval size is the subspace count of the quotient. + quotients[len(fs)] += 1 + profile = given_profile(graph, given) + return { + "max_climb": max_jump, + "edge_max_histogram": dict(sorted(hist.items())), + "edges_below_their_max": increases, + "rank5_minima": dict(sorted(rank5_min.items())), + "free_gates": len(graph["domain"]), + "forced_gates": len(graph["given"]) - len(graph["domain"]), + "interval_sizes": dict(sorted(sizes.items())), + "centre_descents": sorted(graph["centre"]), + "graph_profile": profile, + "quotient_counts": {str(k): v for k, v in sorted(quotients.items())}, + } + + +def certify(w): + with_cones = census(w, True) + without = census(w, False) + walked = section_profile(w) + need(with_cones["graph_profile"] == PROFILE, "graph profile differs from the word") + need(walked == PROFILE, "section walk differs from the word") + need(with_cones["centre_descents"] == [8] * 8, "centre descents") + need(with_cones["max_climb"] == 5, "climb cap") + need(with_cones["free_gates"] == 1741, "free-gate tie-out") + need(with_cones["forced_gates"] == 3672, "forced-gate tie-out") + need(with_cones["interval_sizes"] == {2: 1098, 5: 613, 16: 30}, "interval census") + need(with_cones["edge_max_histogram"][5] == 82, "rank-5 edge multiplicity") + need(with_cones["rank5_minima"] == {3: 24, 4: 26, 5: 32}, "rank-5 minima") + need(sum(with_cones["rank5_minima"].values()) == 82, "rank-5 split") + need(max(with_cones["edge_max_histogram"]) == 5, "histogram support") + need(without["max_climb"] == 5, "cone ceilings are not what cuts rank 6") + # Ambient lemma, independent of the word: a jump inside F2^9 is at most 9. + blank, full = basis(()), basis(FULL) + need(len(full) - len(blank) == 9, "ambient dimension") + need(9 < TARGET_RANK and with_cones["max_climb"] < TARGET_RANK, "rank 44 comparison") + max_paid = max(with_cones["max_climb"], max(with_cones["centre_descents"])) + need(max_paid == 8, "largest paid child rank") + # Controls. Each must reject a weakened reading. + need(not all(d <= 4 for d in with_cones["edge_max_histogram"]), "rank 4 would be a false cap") + try: + basis([1 << H]) + raise ValueError("bit 9 was accepted") + except ValueError as exc: + need("outside F2^9" in str(exc), "outside-vector control") + need(with_cones["edges_below_their_max"] >= 0, "increase count") + result = { + "schema": "selected-k8-child-rank-bound-v1", + "word_sha256": WORD_SHA, + "ambient_dimension": H, + "largest_paid_child_rank": max_paid, + "largest_graph_climb": with_cones["max_climb"], + "centre_descent_rank": 8, + "centre_descent_count": 8, + "rank_44_emitted": False, + "free_gates": with_cones["free_gates"], + "forced_gates": with_cones["forced_gates"], + "interval_sizes": with_cones["interval_sizes"], + "edge_max_histogram": with_cones["edge_max_histogram"], + "edges_whose_jump_can_increase": with_cones["edges_below_their_max"], + "rank5_capable_edges_by_minimum": with_cones["rank5_minima"], + "max_climb_without_cone_ceilings": without["max_climb"], + "given_profile": PROFILE, + "section_walk_agrees": True, + "no_new_kappa": True, + } + return result + + +def main(): + write = "--write" in sys.argv + result = certify(load_word()) + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if write: + RECEIPT.write_text(text) + else: + need(RECEIPT.read_text() == text, "RESULT.json drift") + print( + "PASS_SELECTED_K8_CHILD_RANK_BOUND " + f"max_paid_rank={result['largest_paid_child_rank']} " + f"max_climb={result['largest_graph_climb']} " + f"centre=8x8 rank44=0 free_gates={result['free_gates']} " + f"increasable_edges={result['edges_whose_jump_can_increase']} " + "no_new_kappa" + ) + + +if __name__ == "__main__": + main()