diff --git a/research/p104-owned-coding-boundaries/JOINT-BOUNDARY.md b/research/p104-owned-coding-boundaries/JOINT-BOUNDARY.md new file mode 100644 index 0000000000..7132967f59 --- /dev/null +++ b/research/p104-owned-coding-boundaries/JOINT-BOUNDARY.md @@ -0,0 +1,124 @@ +# A joint moment floor for the complete eight-owned-block boundary + +Source: PR5580 head `6efa248cf456d6101d757e9d09ba29711d18a13a`, compressed word +SHA256 `b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b`. +No new kappa or construction is claimed. + +## The deliberately enlarged boundary + +The replacement interval is `[13378,13485)` in the source program, from the +first owned INIT to just after the last owned CLEAR. Its public boundary has +41 roles: eight distinct copied producers and 33 distinct recipients. No +other public role is read or modified within the literal interval. + +Treat these 41 public entry values as independent coordinates. The verifier +checks that their actual prefix rows have rank41 on original arbitrary public +inputs. It also checks that the fixed suffix observes all41 public coordinates +with column rank41. Therefore an exact whole-word replacement using only these +roles must implement the same local public map: from `S(R-T)P=0`, right and left +inverses imply `R=T`. It may not rely on correlated values in outside registers. + +Every producer enters and exits at dimension8. Every recipient keeps its own +arbitrary input and gains a nonzero multiple of exactly one producer. For each +producer, at least one recipient exits at dimension1. Projection of these eight +observations onto the eight independent producer coordinates has rank8. + +An allowed replacement can change every internal scalar dependency, introduce +arbitrarily many zero-initialized owned fields, share private work across all +eight original lifetimes, and use arbitrary rational scalar operations. It +must preserve all public entry/exit values and frames, clear private outputs, +use common-frame scalar operations, ascending public transports and paid +descending owned transports. It introduces no public helper or new productive +credit. This is stronger than seven separate fixed-star theorems, but weaker +than a global lower bound allowing earlier preparation or outside information. + +## Seven information cuts + +Fix a dimension threshold `k` in `{2,3,4,5,6,7,8}`. Project every current scalar +value onto its eight producer coordinates. Let `V_k` be the span of every such +projected row ever observed in a register with frame dimension less than k. +The span retains past observations after storage is erased or moved away. + +Initially `V_k=0`: the only boundary coordinates containing producer information +are the eight producer registers themselves, all at dimension8. Other input +coordinates are independent recipient values, whose producer projections vanish. + +Scalar combinations at a common frame below k do not enlarge `V_k`. Operations +above k stay above k. INIT is zero, CLEAR cannot add information, and a public +ascent cannot carry information from above the threshold to below it. Only an +owned descent from dimension `a>=k` to `b= c * 7^(t-1). +``` + +For `r<=7`, this follows from `r^(t-1)>=7^(t-1)` and `c<=r`. For `r>=7`, +it follows from `r^t>=7^t` and `c<=7`. Summing over all owned transports and +then summing the seven rank-eight cut requirements gives + +``` +total owned paid moment >= 56 * 7^(t-1) = 8 H7(t). +``` + +The source's public boundary has total ascending dimension change31, spread +over31 fields each changing by one dimension. Every physical public field must +retain its own endpoint. Its required rank-one ascent costs H1, independently +of the owned transports counted above. Thus every replacement pays at least + +``` +31 H1(t) + 8 H7(t). +``` + +The literal word instead pays + +``` +33 H1(t) + H2(t) + H3(t) + 7 H7(t). +``` + +Therefore the maximum possible raw recursive saving inside this full shared +boundary is at most + +``` +2 H1(t) + H2(t) + H3(t) - H7(t). +``` + +Both have the same rank mass87 at t=1. The cap is the exceptional role738's +fragmentation penalty. The argument does not prove this cap attainable; extra +middle-level delivery constraints may make the actual optimum higher. + +## Crucial distinction from original-input dimensions + +The original word's relevant inputs mostly enter on dimension0 or1 frames. +Those original variables do NOT justify dimension cuts requiring eight +high-dimensional sources. The theorem is valid here only because it uses the +later 41-role boundary, treats its coordinates independently (with verified +prefix and suffix ranks), and disallows reading outside public side information. +Moving the boundary earlier can invalidate the source-dimension hypothesis. + +This is not a sum of the nonadditive original-support loss-space bounds. It is +a new joint information-flow argument under a stronger boundary contract. +It gives no unrestricted whole-word tariff optimum, new productive credit, +ordinary-pass improvement, native admission or new multiplication bound. + +## Certificate + +`joint_boundary.py` reconstructs all source scalar rows and frame/lifetime +legality; finds the interval and its41roles; proves both boundary ranks; checks +the exact recipient map, eight one-dimensional independent observations, +public31H1 tariff and each of the seven source crossing counts. A scope control +duplicates one observation and correctly lowers the observation rank to7. + +Prepared with substantial OpenAI Codex assistance. Apache-2.0. Retain the PR5580, +PR5569, PR5561 and complete P104 predecessor attribution in the source package. diff --git a/research/p104-owned-coding-boundaries/PROOF.md b/research/p104-owned-coding-boundaries/PROOF.md new file mode 100644 index 0000000000..c73dbf8167 --- /dev/null +++ b/research/p104-owned-coding-boundaries/PROOF.md @@ -0,0 +1,107 @@ +# Rational recoding and shared-boundary limits for P104 owned values + +All assertions below are about the literal PR5580 word at head +`6efa248cf456d6101d757e9d09ba29711d18a13a`. They do not assert a new +construction, global optimum, native implementation, or multiplication bound. + +## 1. A complete classification of the unchanged producer span + +Let `D_0,...,D_7` be the eight public scalar rows copied into owned fields +735 through 742. Rows are rational covectors on **all 735 arbitrary public +inputs**, including the original zero-frame helper inputs. The verifier +reconstructs the prefix from the identity, rather than assuming those helper +inputs vanish. It confirms that these producer values do not change between +the first owned INIT and their respective COPY events. + +For a covector `x`, define its original-entry support to be the binary span +of the original entry frames of inputs with nonzero coefficient in `x`. +This is a property of its covector, not an assertion that `x` can be built +at that frame with no paid work. + +Every proper subspace of the ambient `F_2^9` lies in a hyperplane `ker(h)` +for some nonzero binary normal `h`. For each of the 511 normals, project +the eight rational covectors onto original input coordinates whose entry +frames are not contained in that hyperplane. A combination `sum a_i D_i` +has support inside the hyperplane exactly when its coefficient vector `a` +is in this projected matrix's rational kernel. + +Exact Fraction elimination gives 495 matrices of rank eight and 16 of rank +seven. The latter have one-dimensional kernels. Every listed kernel mode +has support dimension exactly eight, checked by binary elimination. Hence: + +* No nonzero rational combination of the unchanged producers has + original-entry support dimension at most seven. +* Exactly 16 projective combinations have proper support: the eight + original producers and eight mixed modes listed in RESULT.json. +* Every other nonzero combination has support dimension nine. + +This is an exhaustive rational statement, not a bounded coefficient search. +The independence minor below also excludes a nonzero coefficient vector +representing the zero covector. + +## 2. Direct nested delivery does not remove an original mode + +Let `L_i` be the fixed one-dimensional final delivery frame for `D_i`. +A mode with support hyperplane `ker(h)` can descend directly from that +hyperplane to `L_i` only if `h` annihilates `L_i`. The verifier tests every +one of the sixteen classified modes at every final delivery line. + +After removing `D_i`, exactly three mixed modes remain eligible at `L_i`. +Their coefficient vectors have rational rank three; adjoining the unit +vector for `D_i` raises that rank to four. RESULT.json records an exact +separating functional for each destination, annihilating all three +alternates and taking value one on `D_i`. + +This obstruction survives arbitrary corrections from original inputs +whose entry frame is zero. The eight producer covectors restricted to +nonzero-entry inputs have rank eight, witnessed by the explicitly checked +minor on columns `[0,1,2,4,5,6,9,12]`. Therefore a producer combination is +a zero-entry-input correction only when all eight coefficients vanish. + +This is a direct nested 8-to-1 delivery obstruction in the unchanged producer +span, starting at each mode's original-entry support hyperplane and using +fixed final delivery lines. +It does not rule out earlier owned preparation, intermediate payloads +outside that span, moving through a different recipient schedule, or +changed public dependencies. Nor does an entry-support hyperplane by +itself establish legal preparation of its mixed mode there. + +## 3. Joint transport floor across all eight blocks + +See [JOINT-BOUNDARY.md](JOINT-BOUNDARY.md) for the independent information-cut +argument and full contract. The interval `[13378,13485)` has 41 public +boundary fields: eight producers and 33 distinct recipients. Their entry +rows have rank 41; the unchanged suffix observes their exits with rank 41. +These verified facts force a replacement using only these public fields +to preserve the exact local map. + +The map carries eight independent producer coordinates from dimension-eight +inputs to dimension-one observations. At every dimension threshold 2 through +8, at least eight scalar values must cross downward in owned fields. +Common-frame scalar operations and public ascents cannot create a downward +crossing. The argument allows arbitrary rational dependencies, any number +of zero-initialized owned fields, erasures, and sharing across the blocks. + +For `H_r(t)=r^t`, `0 1}) + need(counts == {8: 495, 7: 16}, 'complete all-511 rational rank census') + need(len(modes) == 16 and sum(m['mixed'] for m in modes) == 8, 'eight original and eight mixed lines') + receipt = {'first_owned_init': first, 'source_roles': [e[2] for _, e in copies], + 'rank_counts': {str(k): v for k, v in sorted(counts.items())}, 'modes': modes, + 'scope': 'Every rational combination of the unchanged eight producer values; original-entry support geometry only.'} + return receipt, modes, producers diff --git a/research/p104-owned-coding-boundaries/delivery.py b/research/p104-owned-coding-boundaries/delivery.py new file mode 100644 index 0000000000..b316373d40 --- /dev/null +++ b/research/p104-owned-coding-boundaries/delivery.py @@ -0,0 +1,171 @@ +"""Exact direct-delivery gate for the supplied P104 sixteen-mode family. + +This does not establish that the family is complete: the all-hyperplane +classification is a separate obligation. Producer covectors must be extracted +independently from the word. This routine verifies their support geometry, the +supplied mixed-mode identities, and all eight quotient-space delivery tests. +""" +from fractions import Fraction as Q + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def rref(rows, width): + a = [[Q(x) for x in row] for row in rows] + need(all(len(row) == width for row in a), "matrix width") + pivots = [] + for col in range(width): + hit = next((j for j in range(len(pivots), len(a)) if a[j][col]), None) + if hit is None: + continue + k = len(pivots) + a[k], a[hit] = a[hit], a[k] + v = a[k][col] + a[k] = [x / v for x in a[k]] + for j in range(len(a)): + if j != k and a[j][col]: + v = a[j][col] + a[j] = [x - v * y for x, y in zip(a[j], a[k])] + pivots.append(col) + if len(pivots) == len(a): + break + return a, pivots + + +def rank(rows, width): + return len(rref(rows, width)[1]) + + +def dot(a, b): + return sum((x * y for x, y in zip(a, b)), Q(0)) + + +def parity_dot(a, b): + return (a & b).bit_count() % 2 + + +def binary_basis(vectors): + basis = {} + for x in vectors: + x = int(x) + while x: + p = x.bit_length() - 1 + if p in basis: + x ^= basis[p] + else: + basis[p] = x + break + return [basis[p] for p in sorted(basis, reverse=True)] + + +def sparse(row): + return {int(i): Q(v) for i, v in row.items() if Q(v)} + + +def mix(coefficients, producers): + out = {} + for a, row in zip(coefficients, producers): + for j, v in row.items(): + out[j] = out.get(j, Q(0)) + a * v + return {j: v for j, v in out.items() if v} + + +def separator(rows, target, n): + unit = [Q(int(j == target)) for j in range(n)] + a, pivots = rref([list(row) + [Q(0)] for row in rows] + [unit + [Q(1)]], n + 1) + need(n not in pivots, "target is in the alternate delivery span") + answer = [Q(0)] * n + for row, p in zip(a, pivots): + answer[p] = row[-1] + need(answer[target] == Q(1), "normalized separator") + need(all(dot(row, answer) == Q(0) for row in rows), "separator annihilates alternates") + return answer + + +def verify_delivery(word, exact_modes, producers): + """Return an exact receipt or raise ValueError; no asserts or float arithmetic. + + Scope: unchanged final payloads in span(D), direct nested 8-to-1 deliveries + starting at each payload's original-entry support, fixed final lines, and + arbitrary free corrections from zero-entry-frame original inputs. Earlier + owned preparation and intermediate components outside span(D) remain open. + """ + n = len(producers) + need(n == 8, "eight supplied source producers") + need(len(exact_modes) == 16, "sixteen supplied projective modes") + frames = word["frames"] + initial = [frames[f] for f in word["initial"]] + ninputs = word["public"] + need(len(initial) == ninputs, "original public input frames") + D = [sparse(p["initial_covector"]) for p in producers] + need(all(0 <= j < ninputs for row in D for j in row), "producer input indices") + nonzero_inputs = [j for j, frame in enumerate(initial) if frame] + projected = [[row.get(j, Q(0)) for j in nonzero_inputs] for row in D] + _, pivot_columns = rref(projected, len(nonzero_inputs)) + need(len(pivot_columns) == n, "producer independence modulo zero-entry inputs") + pivot_inputs = [nonzero_inputs[k] for k in pivot_columns] + minor = [[row.get(j, Q(0)) for j in pivot_inputs] for row in D] + need(rank(minor, n) == n, "explicit quotient independence minor") + + def support(row): + basis = binary_basis(v for j in row for v in initial[j]) + need(len(basis) == 8, "every tested payload has exact eight-dimensional entry support") + normals = [h for h in range(1, 512) if all(parity_dot(h, v) == 0 for v in basis)] + need(len(normals) == 1, "unique ambient-nine hyperplane normal") + return basis, normals[0] + + family = [] + lines = [] + for i, (p, row) in enumerate(zip(producers, D)): + event = word["program"][p["copy_event"]] + need(event == ["COPY", p["owned"], p["source_role"], "1", p["copy_frame"]], "producer COPY metadata") + final_basis = binary_basis(frames[p["clear_frame"]]) + need(len(final_basis) == 1, "fixed one-dimensional delivery frame") + lines.append(final_basis[0]) + basis, normal = support(row) + coeff = [Q(int(i == j)) for j in range(n)] + family.append({"name": f"D{i}", "coefficients": coeff, "normal": normal, "basis": basis}) + seen_original = set() + for m in exact_modes: + coeff = [Q(a) for a in m["coefficients"]] + need(len(coeff) == n and any(coeff), "mixed mode coefficient vector") + row = mix(coeff, D) + basis, normal = support(row) + need(normal == m["normal"], "mixed mode's recomputed entry support normal") + if "covector" in m: + need(row == sparse(m["covector"]), "mixed mode's exact rational covector identity") + original = next((i for i, f in enumerate(family[:n]) if f["coefficients"] == coeff), None) + if original is not None: + need(original not in seen_original, "unique original mode") + need(normal == family[original]["normal"], "original mode support identity") + seen_original.add(original) + else: + family.append({"name": f"E{normal}", "coefficients": coeff, "normal": normal, "basis": basis}) + need(len(seen_original) == n and len(family) == 16, "eight original and eight mixed modes") + need(len({m["normal"] for m in family}) == 16, "sixteen distinct support hyperplanes") + receipt = [] + for i, line in enumerate(lines): + own = family[i] + need(parity_dot(own["normal"], line) == 0, "original producer admits its direct nested delivery") + alternate = [m for m in family if m["name"] != own["name"] and parity_dot(m["normal"], line) == 0] + need(len(alternate) == 3 and all(m["name"].startswith("E") for m in alternate), "exactly three mixed admissible alternates") + rows = [m["coefficients"] for m in alternate] + need(rank(rows, n) == 3, "alternate coefficient rank three") + y = separator(rows, i, n) + unit = [Q(int(j == i)) for j in range(n)] + need(rank(rows + [unit], n) == 4, "target raises admissible rank") + receipt.append({"target": i, "delivery_line": line, + "admissible_alternates": [m["name"] for m in alternate], + "rank": 3, "target_in_span": False, + "separator": [str(v) for v in y]}) + return {"scope": "direct nested 8-to-1 sixteen-mode delivery, modulo zero-entry input corrections", + "quotient_rank": n, "quotient_pivot_inputs": pivot_inputs, + "quotient_minor": [[str(v) for v in row] for row in minor], + "source_normals": [m["normal"] for m in family[:n]], + "mixed_normals": [m["normal"] for m in family[n:]], + "delivery_tests": receipt} + + diff --git a/research/p104-owned-coding-boundaries/inputs/README.md b/research/p104-owned-coding-boundaries/inputs/README.md new file mode 100644 index 0000000000..84d6228229 --- /dev/null +++ b/research/p104-owned-coding-boundaries/inputs/README.md @@ -0,0 +1,20 @@ +# Retained source + +`pr5580-WORD.json.gz` is a byte-identical copy of +`research/p104-event-contact-step/WORD.json.gz` from PR #5580, head +`6efa248cf456d6101d757e9d09ba29711d18a13a`: +https://github.com/CrocSwap/integer-mult-bounds/pull/5580 + +The source construction and event-contact change are by Ali Romman with +substantial OpenAI Codex assistance. This package does not claim those as new. +Retain Joel Pulikkan (@GamingPuzzled)'s PR5569 priced helper handoff and PR5472 +successor mechanism; @DreamingOfClouds's PR5561 free-endpoint word and event +toolkit; @thu-nmrc's PR5551 coupled contacts; Ali Romman's PR5544/5545 complete +caller and source closure; Gareth Davidson, David Arias and Cinna Davis for +the P104 word, coalescing and private reuse; Cinna Davis for the controller; +Jacob Alan Sussman for productive recursion; zxv and Cao Yifan for interval, +compiler and native framework work. Earlier geometry, BIT and analytic source +notices remain in the originating source closure. + +Apache-2.0. The retained word is evidence, not new work. Registered replay +reads this local file and does not download or execute foreign code. diff --git a/research/p104-owned-coding-boundaries/inputs/pr5580-WORD.json.gz b/research/p104-owned-coding-boundaries/inputs/pr5580-WORD.json.gz new file mode 100644 index 0000000000..9434855e7d Binary files /dev/null and b/research/p104-owned-coding-boundaries/inputs/pr5580-WORD.json.gz differ diff --git a/research/p104-owned-coding-boundaries/joint_boundary.py b/research/p104-owned-coding-boundaries/joint_boundary.py new file mode 100644 index 0000000000..d72ad43535 --- /dev/null +++ b/research/p104-owned-coding-boundaries/joint_boundary.py @@ -0,0 +1,199 @@ +"""Exact coupled-owned-block boundary certificate for the frozen PR5580 word. + +The theorem is a fixed 41-public-coordinate boundary theorem. It does not +charge original input frames as though they were eight-dimensional registers. +""" +from fractions import Fraction as Q +from collections import Counter +import copy + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def add(row, source, coefficient): + result = dict(row) + for key, value in source.items(): + out = result.get(key, Q(0)) + coefficient * value + if out: + result[key] = out + else: + result.pop(key, None) + return result + + +def apply(rows, event): + op, dst = event[:2] + if op == 'MOVE': + return + if op in ('INIT', 'CLEAR'): + rows[dst] = {} + elif op == 'ADD': + rows[dst] = add(rows[dst], rows[event[2]], Q(event[3])) + elif op == 'SCALE': + rows[dst] = {key: Q(event[2])*value for key, value in rows[dst].items()} + elif op == 'COPY': + rows[dst] = {key: Q(event[3])*value for key, value in rows[event[2]].items()} + else: + raise ValueError('unknown scalar opcode') + + +def rank(rows): + pivots = {} + for row in rows: + row = dict(row) + while row: + col = min(row) + if col not in pivots: + a = row[col] + pivots[col] = {key: value/a for key, value in row.items()} + break + row = add(row, pivots[col], -row[col]) + return len(pivots) + + +def span(basis): + result = {0} + for vector in basis: + result |= {x ^ vector for x in tuple(result)} + need(len(result) == 1 << len(basis), 'binary basis independent') + return result + + +def observations_rank(observations): + return rank([{int(k):Q(v) for k,v in row.items()} for row in observations]) + + +def verify(word): + public, events, frames = word['public'], word['program'], word['frames'] + need(public == 735, 'frozen public inventory') + n = public+8 + copies = [(i,e) for i,e in enumerate(events) if e[0] == 'COPY'] + need([e[1] for _,e in copies] == list(range(735,743)), 'eight owned producers') + sources = [e[2] for _,e in copies] + need(sources == [173,151,146,133,256,92,9,240], 'frozen source order') + start = next(i for i,e in enumerate(events) if e[0] == 'INIT') + stop = 1+max(i for i,e in enumerate(events) if e[0] == 'CLEAR') + block = events[start:stop] + deliveries = [(start+i,e) for i,e in enumerate(block) if e[0] == 'ADD'] + recipients = [e[1] for _,e in deliveries] + need(len(recipients) == len(set(recipients)) == 33, '33 distinct recipients') + roles = sources+recipients + need(len(set(roles)) == 41, '41 distinct public boundary coordinates') + need(all(e[1] in roles or e[1] >= public for e in block), 'no outside destination') + need(all(e[2] in roles or e[2] >= public for e in block if e[0] in ('ADD','COPY')), + 'no outside public read') + + rows = [{i:Q(1)} for i in range(public)]+[{} for _ in range(8)] + current = list(word['initial'])+[None]*8 + spans = [span(f) for f in frames] + active = set() + entry, exit_frames, prefix = None, None, None + for i,e in enumerate(events): + if i == start: + entry = list(current) + prefix = [dict(rows[r]) for r in roles] + op,r = e[:2] + if op == 'MOVE': + need(current[r] == e[2] and e[4] == (r in active), 'MOVE frame and ownership') + need(spans[e[3]] < spans[e[2]] if e[4] else spans[e[2]] < spans[e[3]], 'nested MOVE direction') + current[r] = e[3] + elif op == 'INIT': + need(r >= public and r not in active, 'fresh owned field') + current[r] = e[2] + active.add(r) + elif op == 'CLEAR': + need(r in active and current[r] == e[2], 'owned CLEAR frame') + current[r] = None + active.remove(r) + else: + need(Q(e[-2]) != 0 and current[r] == e[-1], 'nonzero scalar at current chart') + if op in ('ADD','COPY'): + need(e[2] != r and current[e[2]] == current[r], 'common scalar chart') + if op == 'COPY': + need(r in active and not rows[r], 'COPY into zero owned field') + apply(rows,e) + if i+1 == stop: + exit_frames = list(current) + need(not active and current[:public] == word['final'], 'full frame exit') + for r,row in enumerate(rows): + expected = {r:Q(1)} if r < public else {} + if r-112 in word['live']: + expected[r-112] = Q(1) + need(row == expected, 'full arbitrary-input scalar exit') + need(rank(prefix) == 41, 'independent actual local entry coordinates') + + local = [{} for _ in range(n)] + for j,r in enumerate(roles): + local[r] = {j:Q(1)} + for e in block: + apply(local,e) + need(all(local[r] == {j:Q(1)} for j,r in enumerate(sources)), 'all eight producers unchanged') + need(all(local[r] == {} for r in range(public,n)), 'all private exits zero') + need(all(len(frames[entry[r]]) == len(frames[exit_frames[r]]) == 8 for r in sources), + 'producer entry and exit dimensions eight') + target_sources = {} + for j,r in enumerate(recipients,8): + need(local[r].get(j) == 1 and len(local[r]) == 2, 'recipient keeps arbitrary input plus one producer') + source = next(k for k in local[r] if k != j) + need(source < 8 and local[r][source] != 0, 'nonzero original producer transfer') + target_sources[r] = source + observed_roles = [] + observed = [] + for s in range(8): + role = next((r for r in recipients if target_sources[r] == s and len(frames[exit_frames[r]]) == 1), None) + need(role is not None, 'one one-dimensional observation per producer') + observed_roles.append(role) + observed.append({str(k):str(v) for k,v in local[role].items() if k < 8}) + need(observations_rank(observed) == 8, 'eight independent low-dimensional producer observations') + for k in range(2,9): + need(all(len(frames[entry[r]]) >= k for r in sources), 'no producer coordinate initially below threshold') + need(all(len(frames[exit_frames[r]]) < k for r in observed_roles), 'all observations below threshold') + + suffix = [{} for _ in range(n)] + for j,r in enumerate(roles): + suffix[r] = {j:Q(1)} + for e in events[stop:]: + apply(suffix,e) + need(rank(suffix[:public]) == 41, 'fixed suffix observes every local public coordinate') + + public_hist, owned_hist = Counter(), Counter() + threshold_crossings = {k:0 for k in range(2,9)} + for e in block: + if e[0] != 'MOVE': + continue + a,b = len(frames[e[2]]),len(frames[e[3]]) + (owned_hist if e[4] else public_hist)[abs(a-b)] += 1 + if e[4]: + for k in threshold_crossings: + threshold_crossings[k] += b < k <= a + need(public_hist == {1:31}, 'source public histogram 31H1') + need(owned_hist == {7:7,1:2,2:1,3:1}, 'source owned histogram 7H7+2H1+H2+H3') + need(all(count == 8 for count in threshold_crossings.values()), 'source attains each threshold crossing rank') + public_rank = sum(len(frames[exit_frames[r]])-len(frames[entry[r]]) for r in roles) + need(public_rank == 31, 'public entry-exit rank change 31') + need(all(len(frames[exit_frames[r]])-len(frames[entry[r]]) in (0,1) for r in roles), + 'each physical public field requires at most one rank of ascent') + corrupted = copy.deepcopy(observed) + corrupted[-1] = dict(corrupted[0]) + need(observations_rank(corrupted) == 7, 'duplicate observation reduces the rank bound') + return { + 'status':'PASS_JOINT_41_ROLE_OWNED_MOMENT_FLOOR', + 'events_half_open':[start,stop], 'public_roles':roles, + 'sources':sources,'recipients':recipients, + 'prefix_rank':41,'suffix_rank':41, + 'source_entry_dimensions':[len(frames[entry[r]]) for r in sources], + 'observed_roles':observed_roles,'producer_projection_at_observations':observed, + 'threshold_crossing_count':{str(k):v for k,v in threshold_crossings.items()}, + 'public_paid_histogram':{str(k):v for k,v in sorted(public_hist.items())}, + 'owned_paid_histogram':{str(k):v for k,v in sorted(owned_hist.items())}, + 'theorem_floor':'31 H1(t) + 8 H7(t), 0