diff --git a/research/g20-free-carrier-split-obstruction/PROOF.md b/research/g20-free-carrier-split-obstruction/PROOF.md new file mode 100644 index 0000000000..c6d2f2c762 --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/PROOF.md @@ -0,0 +1,139 @@ +# A free choice of carrier does not expose another G20 split + +## Contract and new claim + +Fix Ali Romman's PR5708 word, `WORD.json.gz`, at +`829d01fc031f7323ffcfa423fdfd1f24dcbe3190`. Its scalar normalized +coordinates, native frame induction and existing helper endpoints are cited +premises. This proof does not establish those source results again. + +A helper group G consists of all retained public helper roles with the same +entrance subspace U and exit subspace V. Fix an event cut and one entire bank +S of fields having the same physical frame F, where V is strictly contained +in F and F is strictly contained in U. Include every field in S, including +main fields and existing owned fields. No member of G need occur in S. +Binary changes of basis at the input, cut and output may use every eligible +coordinate. A split must preserve independence and restore every output +outside G. Adding paid frame changes, changing the scalar word, mixing +boundary groups with different endpoint frames and using address-dependent +coefficients are outside this contract. + +The new finite claim is that all 1,981 distinct eligible contexts with +`S intersect G` empty have zero boundary pairing. There are 46 such contexts +with two nonzero kernel spaces; 45 even have nonzero internal pairing. +Thus the failure is not merely the absence of a scalar pivot or the absence +of available kernel vectors. No free choice of an existing physical carrier +repairs the boundary pairing on this word. + +The executable also obtains zero boundary pairing in all 7,870 contexts, +including the helper-pivot domain reported in PR5708. Those old cases are +context for the expansion, not a separate contribution or supplier audit. + +## The necessary boundary pairing + +Use column states. Let A be the complete normalized prefix map from all +entrance fields to the cut, and let B be the suffix map from that cut to all +exit fields. The maps include the scalar effects of owned erasures. Queries +change physical frames and leave normalized coefficients unchanged under +the cited native contract. + +For a row a supported on S, eligibility means c = a A has no coordinates +outside G. For a column b supported on S, eligibility means d = B b has no +coordinates outside G. The full spaces of such a and b are kernels of the +restrictions of A and B to the complementary boundary coordinates. + +An independent one-coordinate split requires + + a b = 1 and c d = 1. + +The internal equation permits extraction and substitution in a cut basis. +The boundary equation is necessary even if the cut carrier and the boundary +helper pivot are different physical roles. To see this, write h for the +original helper inputs and z for the new independent successor input. +Extracting c h and substituting z along b changes the final helper vector to + + h + d (z - c h). + +This uses the cited identity normalized endpoint on the helper group. The +new combined output is + + (c h, (I - d c) h + d z). + +If c d = 0, the nonzero input pair (h,z) = (d,1) maps to zero. If d = 0, +then the successor input is itself lost. Either case contradicts independent +output jobs. Invertible boundary bases cannot repair this rank loss. +The equation c d = 1 follows for an independent split over F2. +For several simultaneously split coordinates the same argument requires an +invertible boundary pairing matrix; a zero matrix excludes every positive +number of channels. + +The zero-pairing conclusion is unchanged by extending scalars to any field +of characteristic two. The kernel spaces extend by scalar extension, and +the zero bilinear matrix remains zero. Over an extension field the required +one-channel pairing is nonzero and can be normalized to one; it is still +excluded here. + +## What the executable enumerates + +There are 685 fields, 14,794 events and 14,795 event cuts, including both +boundaries. Exact rational reduced row spaces identify 645 physical frame +classes. The retained helper endpoint groups have sizes 413, 1 and 1. +For each group, the checker lists every source frame strictly between its +two endpoints. It does not impose a bank-size or kernel-support cutoff. + +The backward sweep computes the suffix columns. For `ADD d,s`, it applies +`B[:,s] ^= B[:,d]`. For an erasure of d it stores B's old d column, then +sets that column to zero. In the forward sweep it removes one event from the +suffix: ADD is its own inverse, and an erasure restores the stored column. +Prefix rows advance by `A[d,:] ^= A[s,:]` or by setting an erased row to +zero. Frame transitions update the bank partition. At the final boundary +the suffix must be the identity and every frame must equal its declared exit. + +An ADD changes only its one common-frame bank. An erasure, initialization or +query changes only the old and new banks of its destination. Every initial +bank and every changed bank is checked. Other banks retain their exact prefix +rows, suffix columns and membership. Exact keys consisting of group, frame, +slots, prefix rows and suffix columns remove repeated contexts. They do not +merge distinct linear-algebra problems. + +For each context the checker computes bases L and R of the two eligible +kernel spaces. It verifies their defining equations and independence. +Opposite-pivot rank elimination separately checks completeness through +`dim kernel = |S| - rank(restriction)`. It then forms every entry + + C_ij = (L_i A) (B R_j). + +Every C is zero. This certifies the entire eligible spaces by bilinearity, +rather than a bounded-support search for a and b. The result excludes a +necessary equation; there is no delivery cost to optimistically set to zero. + +The output records every count and a deterministic digest of the context +summaries. The source hashes are checked before parsing. The generated +execution receipt separately binds the exact package bytes. + +## Controls and scope + +The checker compares the complete dependency space against literal exhaustive +enumeration for all 512 triples of three-bit rows. A two-role borrowed-carrier +example has a real channel in a bank containing no helper role and must be +accepted. Orthogonal-image, unit-channel and foreign-coordinate controls +separate the boundary and eligibility conditions. All checks use explicit +exceptions and remain enabled under optimized Python. + +This is a finite exact certificate plus a scoped algebraic obstruction. +It supplies neither a global BIT lower bound nor a complete multiplication +theorem. It adds no native word, target, paid saving or kappa. Source native, +compiler, precision, ownership, tape, outer-assembly and the five framework +assumptions remain outside this proof. Independent human and formal +proof-kernel review are unclaimed. + +## Credit + +This contribution was produced by Nick Petalas. Credit Ali Romman for the +PR5679 independent-split construction and its different-physical-role open +question, PR5708's exact final word and helper-pivot census, and PR5609's +prefix/suffix cut method on the older word. The source construction retains +Dugongue, ai-nanachi and the compact436, native, controller, helper, ordinary +and stock lineage cited in those packages. Gaussian elimination, rank-nullity +and bilinear base change are classical. No predecessor executable is imported +and no predecessor credit line is changed. New material is Apache-2.0. diff --git a/research/g20-free-carrier-split-obstruction/README.md b/research/g20-free-carrier-split-obstruction/README.md new file mode 100644 index 0000000000..4b251d573c --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/README.md @@ -0,0 +1,97 @@ +# G20 split obstruction with a free choice of physical carrier + +On the fixed final G20 word of Ali Romman's [PR5708](https://github.com/CrocSwap/integer-mult-bounds/pull/5708), +allowing a cut carrier outside the helper endpoint group exposes no additional +independent split. All **1,981 newly admitted contexts have zero boundary +pairing**. This answers the common-frame part of the different-physical-role +question in [PR5679](https://github.com/CrocSwap/integer-mult-bounds/pull/5679), +Open next question 1. Paid changes of frame and changed words remain open. + +Claim type: finite exact certificate with a scoped algebraic proof. No new +kappa, supplier admission or complete multiplication theorem is claimed. +This contribution was produced by Nick Petalas. + +The prior census required an actual helper-group role in the cut bank. +The new test uses the entire common-frame bank and every helper-only prefix +functional and suffix direction, even when the bank contains no such helper. +Among the 1,981 added contexts, 46 have both kernels nonzero and 45 have a +nonzero internal pairing. All still have zero boundary pairing. A change of +carrier alone cannot make the boundary outputs independent. + +## Evidence and reproduction + +The standalone verifier imports no predecessor executable. It authenticates +the exact source word and frames, covers 14,795 event cuts on 685 fields, +and deduplicates 7,870 exact group/frame linear-algebra contexts. All boundary +pairing matrices are zero. The retained endpoint groups have sizes 413, 1 +and 1. There are 645 rational frame classes. + +Every kernel has equation, independence and opposite-pivot rank-completeness +checks. The 516 controls include exhaustive dependency spaces for 512 small +inputs and a positive split with no helper role in the cut bank. The result +and controls pass under normal and optimized Python. + +From the repository root, the local interpreter path is: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/g20-free-carrier-split-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/g20-free-carrier-split-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/g20-free-carrier-split-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/g20-free-carrier-split-obstruction --check-source-history +``` + +Any CPython 3.12 interpreter can replace that path. Only the standard library +is needed. Expected scientific marker: +`PASS_G20_FREE_CARRIER_SPLIT_OBSTRUCTION`. The context-summary digest is +`ba0e0a6915ab530a5f4f31c8ddcf54055325aaa1521bc7057b776f92d085b276`. +The proof and coverage argument are in [PROOF.md](PROOF.md). + +## Limits and predecessor credit + +The result concerns one unchanged normalized scalar word, the existing +common-frame banks, individual helper endpoint groups and ordinary binary +boundary bases. Its zero matrix also excludes scalar extensions in +characteristic two. Mixed-frame bases, different endpoint groups, added +contacts, address-dependent recoding and a changed word are not excluded. +No native/operator admission, complete caller or recursive price is replayed. +Independent human and formal proof-kernel review are unclaimed. + +Credit Ali Romman for PR5679's split construction and explicit open question, +PR5708's changed word and prior helper-pivot census, and PR5609's cut method +on the older word. Those results are cited and used as specifications, not +audited as the deliverable. The new step is the expanded carrier domain and +its exact boundary obstruction on the final word. Retain the source credit +to Dugongue, ai-nanachi, compact436 and all native, controller, helper, +ordinary and stock predecessors named in those packages. New material is +Apache-2.0. + +## Open next questions + +- Can a paid multi-frame boundary give one nonzero eligible boundary pairing + on this exact word? Start with one frame conversion and its inverse, then + account for the changed query ranks, public targets, routes and restoration. + Neither such a channel nor a favorable complete bill is supplied here. +- Can one changed contact make a nonzero boundary pairing in one of the 46 + new contexts with nonzero kernels? First inspect the exact prefix/suffix + supports at those cuts, then prove the changed endpoint and price it. A + different carrier within the unchanged bank cannot suffice. + +The first steps and blockers are recorded in [TASK.json](TASK.json). + +## Verification design + +All loops have finite source-size bounds. The verifier limits inputs to +16 MiB, fields to 700, events to 20,000, frame dimension to eight, frame +records to 2,000 and distinct contexts to 30,000. It writes no files and +has no recursion, subprocesses, dynamic imports or generated code. Each +function is below 60 lines. Explicit invariant checks remain active with +`-O`. Registered replay uses isolated mode and warnings as errors. + +Python allocates integers, rational values and collections during execution, +so fixed steady-state allocation is a managed-runtime deviation from Power +of Ten rule 3. The source limits, finite elimination widths and context cap +bound the live collections. This command is a bounded research check, not a +long-lived service; a fixed-storage implementation would be a separate +requirement if larger instances are introduced. Interpreter and standard +library internal allocation are not instrumented. The scientific result +is independent of a memory-performance claim. diff --git a/research/g20-free-carrier-split-obstruction/SOURCES.json b/research/g20-free-carrier-split-obstruction/SOURCES.json new file mode 100644 index 0000000000..ebe5f09f4d --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/g20-conjugation-admission/WORD.json.gz", + "usage": "input", + "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639", + "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1" + }, + { + "path": "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json", + "usage": "input", + "git_blob": "9edf8d95b45a9c9c766a956bfcd3c19cf07bc13c", + "sha256": "0d99fc6b8f45c03dfba5252a03dd9e7fe23be3a7593dfe15368e34da6629a654" + }, + { + "path": "research/g20-helper-split/README.md", + "usage": "provenance", + "git_blob": "8e534668c9afa886fb37e9abd38ae8f0e1c78936", + "sha256": "a20ddd3361267c3a26639f9e80f178746d32ec6b3541d0176a743d770e5686a2" + }, + { + "path": "research/g20-helper-split/PROOF.md", + "usage": "provenance", + "git_blob": "1253292326385f8039967d0a4ba94668a710fb1a", + "sha256": "6c9366313dcd72d2986a289e15e2c4b89f8ace8fdedf3d5bd17e6f9d98d8c008" + }, + { + "path": "research/g20-conjugation-admission/README.md", + "usage": "provenance", + "git_blob": "b1655b59134ae7a5734628ba1efef6611b2dcd31", + "sha256": "e443b2fd7b988316953bfc7d21045690ea0d3ce9069ce1a06880f6ccfc7ec054" + }, + { + "path": "research/bit-g20-helper-split-cuts/PROOF.md", + "usage": "provenance", + "git_blob": "c237f3c7deabee3f71ea3c8e2a0fb456b5c57849", + "sha256": "54bd732596db4517a3ee83090edaa4bb94d906d92ef06d674fbf617c832a729a" + } + ] +} diff --git a/research/g20-free-carrier-split-obstruction/TASK.json b/research/g20-free-carrier-split-obstruction/TASK.json new file mode 100644 index 0000000000..747703d01c --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact boundary-pairing obstruction for all common-frame split contexts on PR5708, with the helper-pivot restriction removed.", + "scope_change_reason": "PR5679 explicitly leaves different physical roles open. This takes its common-frame subquestion on PR5708 and returns a negative certificate rather than constructing a new supplier.", + "bottleneck_link": "A free choice of physical carrier cannot expose another productive helper split in this fixed G20 word; a changed contact or paid multi-frame boundary is needed before claiming a moment gain.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified expanded-domain result; do not search changed words or paid interfaces.", + "outcome": "negative-result", + "evidence": "PROOF.md and standalone verify.py: 1,981 added contexts, 46 with two nonzero kernels, zero boundary pairing in every case; 516 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a paid multi-frame boundary expose one nonzero helper pairing on this exact word?", + "why_it_matters": "That changes the common-frame hypothesis excluded here.", + "first_step": "Specify one native frame conversion and its inverse at an exact cut, then derive the pairing and full paid/target delta.", + "blocked_by": "No such physical channel, routes, restoration or favorable complete invoice is supplied." + }, + { + "question": "Can a changed contact make a nonzero boundary pairing in one of the 46 added contexts with two nonzero kernels?", + "why_it_matters": "A changed prefix/suffix can alter the zero boundary matrix.", + "first_step": "Inspect one exact kernel-support pair, change one legal contact, and prove the new independent endpoint.", + "blocked_by": "The unchanged-word obstruction supplies no changed native endpoint or complete bill." + } + ] +} diff --git a/research/g20-free-carrier-split-obstruction/VERIFY.json b/research/g20-free-carrier-split-obstruction/VERIFY.json new file mode 100644 index 0000000000..bed817708a --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/g20-conjugation-admission/WORD.json.gz", + "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate both source inputs; enumerate all cut banks without a helper-pivot restriction; check complete kernels and zero boundary pairing; run exhaustive kernel and positive/negative channel controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the full finite certificate and controls with optimization enabled." + } + ] +} diff --git a/research/g20-free-carrier-split-obstruction/verify.py b/research/g20-free-carrier-split-obstruction/verify.py new file mode 100644 index 0000000000..13326f5900 --- /dev/null +++ b/research/g20-free-carrier-split-obstruction/verify.py @@ -0,0 +1,306 @@ +"""Exact expanded-domain G20 cut obstruction, produced by Nick Petalas. + +The cut contract is due to Ali Romman, PR5679/5708 and PR5609. +This standalone implementation imports no predecessor executable. Apache-2.0. +""" +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +import hashlib +import itertools +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = "research/g20-conjugation-admission/WORD.json.gz" +FRAMES = "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json" +MAX_FIELDS = 700 +MAX_EVENTS = 20000 +MAX_CONTEXTS = 30000 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(rows): + """Unique rational row space, at most sixteen rows and eight columns.""" + basis = {} + for source in rows: + row = list(map(Fraction, source)) + for pivot in sorted(basis): + factor = row[pivot] + row = [x - factor*y for x, y in zip(row, basis[pivot])] + pivot = next((i for i, x in enumerate(row) if x), None) + if pivot is None: + continue + factor = row[pivot] + row = [x / factor for x in row] + for old in tuple(basis): + factor = basis[old][pivot] + basis[old] = [x - factor*y for x, y in zip(basis[old], row)] + basis[pivot] = row + return tuple(tuple(row) for _, row in sorted(basis.items())) + + +def dependencies(rows): + """A basis of all binary row dependencies, retaining coefficients.""" + basis, result = {}, [] + width = max((row.bit_length() for row in rows), default=0) + for i, source in enumerate(rows): + row, coefficients = source, 1 << i + for _ in range(width + 1): + if not row: + result.append(coefficients) + break + pivot = row.bit_length() - 1 + if pivot not in basis: + basis[pivot] = row, coefficients + break + old, combination = basis[pivot] + row ^= old + coefficients ^= combination + else: + raise ValueError("dependency elimination bound") + return result + + +def rank_low(rows): + """Rank with the opposite pivot order and no dependency bookkeeping.""" + basis = {} + width = max((row.bit_length() for row in rows), default=0) + for source in rows: + row = source + for _ in range(width + 1): + if not row: + break + pivot = (row & -row).bit_length() - 1 + if pivot not in basis: + basis[pivot] = row + break + row ^= basis[pivot] + else: + raise ValueError("rank elimination bound") + return len(basis) + + +def combine(rows, coefficients): + value = 0 + require(coefficients.bit_length() <= len(rows), "coefficient width") + for i, row in enumerate(rows): + if coefficients >> i & 1: + value ^= row + return value + + +def eligible(rows, outside): + masked = [row & outside for row in rows] + kernel = dependencies(masked) + require(len(kernel) == len(rows) - rank_low(masked), "kernel dimension") + require(rank_low(kernel) == len(kernel), "kernel independence") + require(all(combine(masked, x) == 0 for x in kernel), "kernel equations") + return kernel, [combine(rows, x) for x in kernel] + + +def pairings(prefix, suffix, outside): + left, inputs = eligible(prefix, outside) + right, outputs = eligible(suffix, outside) + boundary = [sum(((c & d).bit_count() & 1) << j + for j, d in enumerate(outputs)) for c in inputs] + internal = [sum(((a & b).bit_count() & 1) << j + for j, b in enumerate(right)) for a in left] + return len(left), len(right), rank_low(boundary), rank_low(internal) + + +def geometry(frames): + require(1 <= len(frames) <= 2000, "frame inventory bound") + for entry in frames.values(): + require(0 <= entry["dim"] <= 8, "frame dimension bound") + require(len(entry["B"]) == entry["dim"], "frame row count") + require(all(len(row) == 8 for row in entry["B"]), "frame width") + spaces = {int(i): canonical(entry["B"]) for i, entry in frames.items()} + shapes = sorted(set(spaces.values())) + labels = {i: shapes.index(space) for i, space in spaces.items()} + labels[None] = None + return labels, shapes + + +def group_contract(word, labels, shapes, helper_begin): + groups = defaultdict(set) + owned = set(word["owned"]) + for h in range(helper_begin, len(word["start"])): + if h not in owned: + groups[labels[word["start"][h]], labels[word["final"][h]]].add(h) + compatible = defaultdict(list) + masks = {} + full = (1 << len(word["start"])) - 1 + for group, members in groups.items(): + entrance, exit_frame = group + masks[group] = full ^ sum(1 << h for h in members) + for f, shape in enumerate(shapes): + if not len(shapes[exit_frame]) < len(shape) < len(shapes[entrance]): + continue + if canonical(shapes[entrance] + shape) != shapes[entrance]: + continue + if canonical(shape + shapes[exit_frame]) == shape: + compatible[f].append(group) + return groups, compatible, masks + + +def suffix_start(events, n): + columns = [1 << i for i in range(n)] + erased = {} + for k in reversed(range(len(events))): + event = events[k] + op, d = event[:2] + if op == "ADD": + columns[event[2]] ^= columns[d] + elif op == "ERASE": + erased[k] = columns[d] + columns[d] = 0 + return columns, erased + + +def inspect_bank(f, cut, state, banks, prefix, suffix, contract, seen, counts, digest): + groups, compatible, masks = contract + if f not in compatible or not banks[f]: + return + slots = tuple(sorted(banks[f])) + aa, bb = tuple(prefix[i] for i in slots), tuple(suffix[i] for i in slots) + for group in compatible[f]: + key = group, f, slots, aa, bb + if key in seen: + continue + require(len(seen) < MAX_CONTEXTS, "context resource bound") + seen.add(key) + ldim, rdim, boundary_rank, internal_rank = pairings(aa, bb, masks[group]) + free_carrier = not (set(slots) & groups[group]) + counts["contexts"] += 1 + counts["without_helper_slot"] += int(free_carrier) + counts["both_kernels_nonzero"] += int(ldim > 0 and rdim > 0) + counts["boundary_nonzero"] += int(boundary_rank > 0) + counts["internal_nonzero"] += int(internal_rank > 0) + if free_carrier: + counts["new_both_kernels_nonzero"] += int(ldim > 0 and rdim > 0) + counts["new_boundary_nonzero"] += int(boundary_rank > 0) + counts["new_internal_nonzero"] += int(internal_rank > 0) + record = [cut, list(group), state[slots[0]], list(slots), + ldim, rdim, boundary_rank, internal_rank, free_carrier] + digest.update((json.dumps(record, separators=(",", ":")) + "\n").encode()) + + +def move(event, k, prefix, suffix, erased, state, labels, banks): + op, d = event[:2] + before = labels[state[d]] + touched = {before} + if op == "ADD": + source, frame = event[2:] + require(state[d] == state[source] == frame, "literal ADD common frame") + prefix[d] ^= prefix[source] + suffix[source] ^= suffix[d] + elif op in ("ERASE", "INIT", "Q", "ZERO_Q"): + if op == "ERASE": + prefix[d] = 0 + suffix[d] = erased[k] + if op in ("Q", "ZERO_Q"): + require(state[d] == event[2], "query entrance") + state[d] = event[3] + else: + state[d] = event[2] + banks[before].remove(d) + banks[labels[state[d]]].add(d) + touched.add(labels[state[d]]) + else: + raise ValueError("unknown event") + return touched + + +def scan(word, labels, shapes, helper_begin=222): + n, events = len(word["start"]), word["records"] + require(1 <= n <= MAX_FIELDS and len(events) <= MAX_EVENTS, "word bounds") + require(len(word["final"]) == n, "boundary lengths") + for event in events: + require(2 <= len(event) <= 5 and 0 <= event[1] < n, "event destination") + if event[0] == "ADD": + require(len(event) == 4 and 0 <= event[2] < n, "ADD source") + contract = group_contract(word, labels, shapes, helper_begin) + prefix = [1 << i for i in range(n)] + suffix, erased = suffix_start(events, n) + state = word["start"][:] + banks = defaultdict(set) + for i, frame in enumerate(state): + banks[labels[frame]].add(i) + counts, seen, digest = Counter(), set(), hashlib.sha256() + for f in sorted(f for f in banks if f is not None): + inspect_bank(f, -1, state, banks, prefix, suffix, contract, seen, counts, digest) + for k, event in enumerate(events): + touched = move(event, k, prefix, suffix, erased, state, labels, banks) + for f in sorted(f for f in touched if f is not None): + inspect_bank(f, k, state, banks, prefix, suffix, contract, seen, counts, digest) + require(state == word["final"], "cut traversal reaches declared frames") + require(suffix == [1 << i for i in range(n)], "suffix traversal closure") + return dict(counts), digest.hexdigest(), contract[0] + + +def controls(): + checked = 0 + for rows in itertools.product(range(8), repeat=3): + kernel = dependencies(rows) + exhaustive = [x for x in range(8) if combine(rows, x) == 0] + generated = {combine(kernel, x) for x in range(1 << len(kernel))} + require(generated == set(exhaustive), "exhaustive dependency control") + checked += 1 + # A genuine nonhelper carrier: swap an arbitrary helper into the borrowed + # role, cross the intermediate frame there, return and undo the swap. + shapes = [(), ((Fraction(1),) + (Fraction(0),)*7,), + tuple(tuple(Fraction(i == j) for j in range(8)) for i in range(8))] + labels = {0: 0, 1: 1, 2: 2, None: None} + swap = [["ADD", 0, 1, 2], ["ADD", 1, 0, 2], ["ADD", 0, 1, 2]] + word = {"start": [2, 2], "final": [0, 2], "owned": [1], + "records": swap + [["Q", 1, 2, 1, 7], ["Q", 1, 1, 2, 7]] + + swap + [["Q", 0, 2, 0, 8]]} + result, _, _ = scan(word, labels, shapes, 0) + require(result["new_boundary_nonzero"] == 1, "true outside-carrier accepted") + require(pairings([1], [2], 0)[2] == 0, "orthogonal nonzero images") + require(pairings([1], [1], 0)[2] == 1, "unit boundary channel") + require(pairings([1], [1], 1)[2] == 0, "foreign-coordinate exclusion") + return checked + 4 + + +def load_sources(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + expected = {row["path"]: row["sha256"] for row in manifest["files"] + if row["usage"] == "input"} + require(set(expected) == {WORD, FRAMES}, "exact two-input boundary") + payloads = {} + for path in (WORD, FRAMES): + raw = (ROOT / path).read_bytes() + require(len(raw) <= 16 * 1024 * 1024, "input size bound") + require(hashlib.sha256(raw).hexdigest() == expected[path], "source hash " + path) + decoded = gzip.decompress(raw) if path.endswith(".gz") else raw + require(len(decoded) <= 16 * 1024 * 1024, "decoded input bound") + payloads[path] = json.loads(decoded) + return payloads[WORD], payloads[FRAMES]["frames"] + + +def main(): + word, frames = load_sources() + labels, shapes = geometry(frames) + count_controls = controls() + counts, digest, groups = scan(word, labels, shapes) + require(counts["boundary_nonzero"] == 0, "zero boundary pairing at every context") + report = {"claim_type": "finite exact certificate and scoped algebraic obstruction", + "fields": len(word["start"]), "events": len(word["records"]), + "all_cuts": len(word["records"]) + 1, + "frame_classes": len(shapes), + "helper_group_sizes": sorted(map(len, groups.values())), + "counts": counts, "controls": count_controls, + "context_digest": digest} + print(json.dumps(report, sort_keys=True, indent=2)) + print("PASS_G20_FREE_CARRIER_SPLIT_OBSTRUCTION") + + +if __name__ == "__main__": + main()