diff --git a/research/seven-source-distinct-axis-obstruction/PROOF.md b/research/seven-source-distinct-axis-obstruction/PROOF.md new file mode 100644 index 0000000000..bd4569b11a --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/PROOF.md @@ -0,0 +1,158 @@ +# Seven distinct source axes cannot supply the seven-source connector + +This scoped obstruction was produced by Nick Petalas. Apache-2.0. +The finite exclusion below is new. The normalized-axis and mandatory-mask +methods are credited to conorholds, Mason Hale and Arham Tahir. + +## 1. Contract and conclusion + +There are seven immutable source rows x_j, four arbitrary dirty root rows z_p, +and separate output rows y_m for every nonzero seven-bit mask m. Source calls +add B_j x_j to one physical root. Output calls add A_m z_p to their own target. +Every B_j and A_m occurs exactly twice. The compatible binary linear maps are +arbitrary, including singular and noncommuting maps. Outputs are not observed +or used as scratch. All roots and sources restore. Child scratch is private +and restores under its inherited contract. + +Allow any finite number of invertible scalar binary root-frame changes, any +physical port on each call, and no bound on the cost of those changes. Granting +these operations only enlarges a paid-XOR interface. + +**Theorem.** A universal connector under this contract cannot have seven +pairwise distinct normalized source axes. If it supplies the all-ones output +and its normalized axes are distinct, at least 22 other requested masks fail +the mandatory-mask necessary condition. The number 22 is the exact minimum +of that deficit in the complete reduced domain. It is not an exact maximum +for the total set of outputs a legal circuit can supply. + +Consequently a universal seven-source connector with four dirty roots must +repeat an axis. This is a restriction within the known optimal root count, +not a new root-count theorem or a transfer-count minimum. + +## 2. Necessary mask equation + +Let R_t be the invertible matrix carrying the four independent initial dirt +rows into the current roots. In normalized coordinates a source call at port p +injects the nonzero column R_t^{-1} e_p. Its two calls must have the same +normalized column v_j, since no other call can remove that source coefficient +from the restored roots. Final dirt restoration also forces R_final=I. + +Let q_t be the seven-bit parity of source calls before a cut. A physical root +whose dirty covector is r then contains + + r z_initial + sum_j (r v_j) q_t[j] B_j x_j. + +Two calls of an arbitrary A_m cancel initial dirt only when their dirty +covectors agree. Their source mask is therefore + + m = h AND d, h = r V, d = q_s XOR q_t, V=[v_0 ... v_6]. + +Write H=rowspace(V) and D(w)={q_s XOR q_t} for the paired source word w. +Thus every supplied mask belongs to {h AND d: h in H, d in D(w)}. +This implication is the normalized-axis method of PR2182 and the code +formulation of PR2795. The calculation above states the exact premise used +here; neither predecessor's census or attaining construction is reverified. + +The implication is necessary already for identity source/output maps on +independent scalar inputs. Hence it applies at every positive row length, +without inferring arbitrary-size behavior from a finite dense fixture. + +## 3. Complete domain for distinct axes + +The all-ones mask requires both h=127 and d=127. Some nonzero covector r_* +therefore has r_* v_j=1 for every j. The axes lie in an eight-point affine +hyperplane of F2^4. Under the distinctness hypothesis they occupy seven of +its points and span F2^4. + +A change of root basis takes this hyperplane to the points (1,u), u in F2^3. +The affine transformations u -> Au+b act transitively on its omitted point +and are induced by invertible linear maps on (1,u). We may choose the omitted +point to be u=7. Coordinate assignments to the seven sources remain arbitrary. +Therefore every possible H is a coordinate permutation of + + H_0 = { ((r dot (1,j)))_(j=0,...,6) : r in F2^4 }. + +Here (1,j) is encoded by 1|(j<<1). The primary generator visits all 7! +coordinate permutations, takes their exact row spaces, and deduplicates them. +There are exactly 30 distinct codes, each with sixteen words. No source-order +symmetry is assumed after this code inventory is formed. + +For every proper codeword h != 127 define its supported subsets. A nonzero +mask m is mandatory when no such h contains its support. If m=h AND d is +mandatory, h must be 127, so d=m. Thus + + M(H) subset D(w) + +is necessary for universality. Each of the thirty codes has exactly 57 +mandatory masks, as directly enumerated in both checkers. + +## 4. Complete source-order reduction + +The equality d=127 means an interval of the paired source word contains each +source an odd number of times. Since there are only two calls per source, +that interval contains each source exactly once and has length seven. +Rotate the closed source word to start at that interval and rename sources +in its order. The resulting word is + + 0,1,2,3,4,5,6, permutation(0,1,2,3,4,5,6). + +Rotation translates all prefix parities by the same vector and preserves D. +Renaming coordinates permutes H as well as D. Enumerating all 5,040 second +orders and all thirty codes is therefore complete for this necessary test. +This is the all-ones interval reduction of PR2795. It does not assert that +physical frame changes can be rotated without paying for them. + +## 5. New finite certificate + +For every reduced pair the checker computes the full bitset M(H) minus D(w). +The two engines agree on every one of the 151,200 bitsets. Their minimum +cardinality is 22, attained by four reduced pairs. There are no zero-deficit +pairs. The generated report contains the complete deficit histogram and a +SHA256 digest of all bitsets in lexicographic (source order, code) order. + +One attaining deficit witness has second order + + 1,4,0,3,6,2,5 + +and code + + 0,11,22,29,37,46,51,56,71,76,81,90,98,105,116,127. + +Its missing mandatory masks are + + 23,45,53,54,55,57,58,61,75,78,79,85,86,87,92,94,102, + 113,117,118,119,121. + +The primary engine uses coordinate permutations of the affine-cube code, +pairwise prefix XORs and support containment. The second enumerates all +11,811 three-dimensional binary RREF row spaces, retains the thirty whose +nonzero vectors all have weight four, and takes orthogonal complements. +It forms D by contiguous interval parities and M by enumerating proper +codeword subsets. The full code inventories and every deficit agree. +No predecessor executable, stored numerical receipt or search solver is an +acceptance input. + +## 6. Consequence and limits + +The 22 absent mandatory masks cannot be recovered by more scalar frame +changes, different physical read ports or a more expensive frame itinerary. +Thus the complete 127-mask endpoint is impossible with distinct axes. If the +all-ones mask is supplied, at most 105 nonzero masks can pass this necessary +test. Attainment of that total-output bound is unclaimed. + +Repeated axes escape the premise. As a positive control, the credited star's +axes (1,1,1,1,2,4,8) and source word + + 0,1,0,1,4,5,6,2,3,2,3,4,5,6 + +pass the full mask-intersection criterion. This is a tiny control on the +scope, not a new verification claim for its physical construction or invoice. +The predecessor's four-root, 56-X star and root-minimum proof remain credited +premises. No smaller paid word was established here. + +Extra source/output calls, source mutation, output feedback, clean roots, +matrix-valued root transformations and nonlinear updates change the contract. +Physical hosting, native realization, tape/precision/stock costs and supplier +admission are not supplied. All five selected framework assumptions remain. +The finite certificate supports this scoped written proof; independent human +and formal proof-kernel review are unclaimed. diff --git a/research/seven-source-distinct-axis-obstruction/README.md b/research/seven-source-distinct-axis-obstruction/README.md new file mode 100644 index 0000000000..02c3d01bc4 --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/README.md @@ -0,0 +1,107 @@ +# Seven-source connectors must repeat a normalized source axis + +This contribution was produced by Nick Petalas. Apache-2.0. + +A universal seven-source connector with four arbitrary dirty roots cannot +assign seven distinct normalized axes to its twice-called source maps. This +is a scoped obstruction with an exhaustive finite certificate. It excludes +an axis-diversity route toward Mason Hale's open transfer-cost question, +without changing the selected frontier or kappa. + +The complete reduced domain contains thirty affine-cube codes and 5,040 +source orders. Every one of the 151,200 pairs misses at least 22 of its 57 +mandatory masks. The minimum deficit 22 is attained by four pairs. It is +sharp for this necessary-condition census, not an exact total-output capacity. +If the all-ones output is supplied, at most 105 nonzero masks pass the test. + +[PROOF.md](PROOF.md) gives the arbitrary-input reduction, complete domain and +an attaining deficit witness. The program grants arbitrarily many scalar +binary root frames and every physical read port, so unpaid frame restrictions +do not cause the exclusion. Every source and output map must occur exactly +twice; sources and roots restore and outputs remain unobserved. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/seven-source-distinct-axis-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/seven-source-distinct-axis-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/seven-source-distinct-axis-obstruction --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter. Direct replay +prints a generated JSON receipt with status +`PASS_SEVEN_SOURCE_DISTINCT_AXIS_OBSTRUCTION`, the full deficit histogram, +minimum witness, census digest and hashes of every package file. It writes +nothing. Normal and optimized modes are registered. + +Two separately implemented code generators, mandatory-set constructions and +word-difference engines agree on every missing-mask bitset. The secondary +code generator examines all 11,811 three-dimensional binary RREF spaces. +Controls cover fourteen cyclic rotations, all 21 coordinate transpositions, +the repeated-axis star positive case, two invalid-word rejections and four +false-variant boundaries. +The two cited main-tree documents are hash authenticated before enumeration. +These are two implementations by one contributor, not independent review. + +The current selected binding control and the card's 945-pairing positive +control pass. No predecessor scientific census is replayed as this result. + +## Source, scope and credit + +Base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8; +selected conditional kappa remains 0.003125804. Exact document pins are in +[SOURCES.json](SOURCES.json). The original card and changed scope are in +[TASK.json](TASK.json). + +- Mason Hale / [PR2282](https://github.com/CrocSwap/integer-mult-bounds/pull/2282) + poses the four-root transfer question and proves the seven-source root minimum. +- Arham Tahir / [PR2795](https://github.com/CrocSwap/integer-mult-bounds/pull/2795) + supplies the code formulation, mandatory masks and all-ones interval reduction. + Its eight-source exclusion and seven-source three-root calibration are different + finite domains from the four-root distinct-axis domain here. +- conorholds / [PR2182](https://github.com/CrocSwap/integer-mult-bounds/pull/2182) + supplies normalized axes, the dirty-root contract and the 56-X attaining star. + Ross Richardson / PR934/943, Douglas Colkitt / PR1185 and their retained + connector, common-factor and compiler lineage retain credit. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372499) +aimed for fewer transfers. The [finding](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372766) +records the delivered narrower obstruction. No shorter word or global transfer +minimum was established. Construction search stopped at this first proved step. + +The main/merged/open searches used the source object, distinct normalized axes, +affine-cube codes and mandatory-mask deficits. The overlap cache covered 550 +open PRs and 6,574 Discussion records; sparse local notes and unpublished work +remain limits. No global literature-priority claim is made for classical +binary code geometry or the credited reductions. + +## Open next questions + +- Can a repeated-axis four-root program use fewer than 56 paid XORs while + retaining all minimum map incidences? First choose one repeated-axis code + and emit its complete frame/source/readout itinerary. A cheaper legal word + and its complete physical port bill remain missing. +- Can a structural argument replace this 151,200-case distinct-axis census? + Start with the 57 mandatory supports and a double-permutation source word. + A uniform interval argument, rather than sampled orders, is needed. + +No new supplier, physical caller, complete multiplication theorem, independent +human review or formal-kernel proof is claimed. Native, compiler, ownership, +stock, precision/tape and analytic transfer obligations remain open. + +## Implementation bounds + +Every loop is bounded by a fixed finite domain: seven coordinates, sixteen +codewords, 128 masks, 5,040 orders, thirty codes or the 11,811 RREF spaces. +Functions are under sixty lines; checks use exceptions and survive `-O`. +There is no recursion, solver, runtime network call or generated executable. +The two census lists have exactly 151,200 integers of at most 128 bits each. + +Power-of-Ten rule 3 has a managed-runtime deviation for Python allocation in +these bounded lists, sets and exact integers. The interpreter allocator is not +inspected. Fixed domain sizes bound live mathematical storage; both lists are +released on process exit. A fixed-capacity implementation would be needed +before reuse in a long-lived service. Warning-strict normal and optimized +commands provide the applicable interpreted-code diagnostics. diff --git a/research/seven-source-distinct-axis-obstruction/SOURCES.json b/research/seven-source-distinct-axis-obstruction/SOURCES.json new file mode 100644 index 0000000000..5ab9c06f6f --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/SOURCES.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/eight-source-root-code/README.md", + "usage": "input", + "git_blob": "ce5d5add72a7b57bb17cc339d9fda4bb0592160c", + "sha256": "8a9100409033acfc0ede9fa260c0172c958e5103a244b1de97b7e132659038d0" + }, + { + "path": "research/seven-source-root-minimum/README.md", + "usage": "input", + "git_blob": "2fac5ab937d94856e55fd753d067f2f6f8ada111", + "sha256": "17554797cf3a8752ef3f8b65b0d7fc9e98f7f99f3afb5dbb1b0952fbf9f1fd58" + } + ], + "predecessor_context": [ + { + "pr": 2282, + "author": "mason-hale", + "original_head": "74e57135608dade29029a1107fdfceec8419c932", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2282", + "usage": "Bibliography only. The replay inputs above are retained main-tree documents, not these separate Git objects." + }, + { + "pr": 2795, + "author": "Arham-Tahir64", + "original_head": "fad52f9528cfea1c3bcfc0094ff56abf945d31a7", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2795", + "usage": "Bibliography only. The replay inputs above are retained main-tree documents, not these separate Git objects." + }, + { + "pr": 2182, + "author": "conorholds", + "original_head": "dc252de1cc594829c3031abdb4de104713bc474a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2182", + "usage": "Bibliography only. The replay inputs above are retained main-tree documents, not these separate Git objects." + } + ] +} diff --git a/research/seven-source-distinct-axis-obstruction/TASK.json b/research/seven-source-distinct-axis-obstruction/TASK.json new file mode 100644 index 0000000000..d087c1b827 --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Exclude seven pairwise distinct normalized source axes in the universal seven-source four-dirty-root paired-call connector; certify the sharp mandatory-mask deficit 22 over all 151200 reduced code/order pairs.", + "scope_change_reason": "The live PR2282 transfer-cost question replaces the card alphabet-extension experiment. The advance claim sought a shorter word. The first proved new step instead excludes the distinct-axis route in the same paid alphabet; the transfer minimum remains open.", + "bottleneck_link": "Interface side result: a cheaper minimum-incidence connector must repeat source axes. No actual selected caller or favorable complete physical bill is supplied, and no kappa changes.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved obstruction and package it. Do not expand the source count, seek a stronger capacity claim or continue searching for a shorter word.", + "outcome": "completed", + "evidence": "PROOF.md and both exact census methods in verify.py; every one of the 151200 missing-mask bitsets agrees; minimum deficit 22 attained four times.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a repeated-axis four-root program beat 56 paid root XORs at minimum map incidences?", + "why_it_matters": "The new obstruction requires an axis repetition, but supplies no better transfer word.", + "first_step": "Fix a repeated-axis code and emit all sources, frame changes and equal-dirt readout pairs.", + "blocked_by": "A shorter arbitrary-input word and a complete physical port/hosting bill." + }, + { + "question": "Can a structural interval argument replace the finite distinct-axis census?", + "why_it_matters": "It would remove a finite computational proof dependency without changing the scoped claim.", + "first_step": "Relate the 57 mandatory supports to the two permutation halves of the source word.", + "blocked_by": "No uniform interval-count argument is provided." + } + ] +} diff --git a/research/seven-source-distinct-axis-obstruction/VERIFY.json b/research/seven-source-distinct-axis-obstruction/VERIFY.json new file mode 100644 index 0000000000..8255f02bdd --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/eight-source-root-code/README.md", + "research/seven-source-root-minimum/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete 151200-case missing-mask agreement between two independently structured finite engines, sharp deficit witness, scope controls and source authentication." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete 151200-case missing-mask agreement between two independently structured finite engines, sharp deficit witness, scope controls and source authentication." + } + ] +} diff --git a/research/seven-source-distinct-axis-obstruction/verify.py b/research/seven-source-distinct-axis-obstruction/verify.py new file mode 100644 index 0000000000..5fd32e96db --- /dev/null +++ b/research/seven-source-distinct-axis-obstruction/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact distinct-axis obstruction, produced by Nick Petalas. Apache-2.0.""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations, permutations +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +N = 7 +UNIVERSE = (1 << 128) - 1 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def span(generators): + values = [0] + for generator in generators: + values += [old ^ generator for old in values] + return tuple(sorted(values)) + + +def axis_codes(): + """Permute the seven points (1,j), j=0,...,6, in the affine cube.""" + base = tuple(sum(((row & (1 | (j << 1))).bit_count() % 2) << j + for j in range(N)) for row in range(16)) + codes = set() + for order in permutations(range(N)): + code = tuple(sorted(sum(((word >> order[j]) & 1) << j + for j in range(N)) for word in base)) + codes.add(code) + return tuple(sorted(codes)) + + +def orthogonal_codes(): + """Separate domain generator: enumerate binary RREF three-row matrices.""" + codes = set() + rref_count = 0 + for pivots in combinations(range(N), 3): + free = [(row, col) for row in range(3) for col in range(N) + if col not in pivots and col > pivots[row]] + for assignment in range(1 << len(free)): + rows = [1 << col for col in pivots] + for bit, (row, col) in enumerate(free): + if assignment & (1 << bit): + rows[row] |= 1 << col + rref_count += 1 + dual = span(rows) + if any(word.bit_count() != 4 for word in dual if word): + continue + code = tuple(word for word in range(128) + if all((word & row).bit_count() % 2 == 0 for row in rows)) + codes.add(code) + need(rref_count == 11811, 'Complete three-dimensional RREF domain') + return tuple(sorted(codes)) + + +def mandatory_scan(code): + return sum(1 << mask for mask in range(1, 128) + if not any(word != 127 and mask & ~word == 0 for word in code)) + + +def mandatory_subsets(code): + allowed = 1 # Empty support is contained in every proper codeword. + for word in code: + if word == 127: + continue + positions = [j for j in range(N) if word & (1 << j)] + for choice in range(1 << len(positions)): + mask = sum(1 << col for j, col in enumerate(positions) + if choice & (1 << j)) + allowed |= 1 << mask + return UNIVERSE ^ allowed + + +def prefix_differences(order): + parity, points = 0, [0] + for label in tuple(range(N)) + order: + parity ^= 1 << label + points.append(parity) + need(parity == 0, 'Paired source restoration') + return sum(1 << mask for mask in {a ^ b for a in points for b in points}) + + +def interval_differences(order): + word = tuple(range(N)) + order + result = 1 + for start in range(14): + parity = 0 + for end in range(start, 14): + parity ^= 1 << word[end] + result |= 1 << parity + return result + + +def census(codes, secondary=False): + """Return every missing-mask set, in lexicographic order of (order,code).""" + mandatory = tuple(mandatory_subsets(code) if secondary else mandatory_scan(code) + for code in codes) + need(all(bits.bit_count() == 57 for bits in mandatory), 'Mandatory-set sizes') + results, histogram = [], Counter() + minimum, witness = 128, None + for order in permutations(range(N)): + differences = (interval_differences(order) if secondary + else prefix_differences(order)) + need(differences & (1 << 127), 'Normalized all-ones interval') + for code, required in zip(codes, mandatory): + missing = required & ~differences + results.append(missing) + count = missing.bit_count() + histogram[count] += 1 + if count < minimum: + minimum = count + witness = {'second_order': list(order), 'code': list(code), + 'missing_masks': [m for m in range(128) if missing >> m & 1]} + need(len(results) == 151200, 'Complete order/code product') + return results, dict(sorted(histogram.items())), minimum, witness + + +def missing_for_word(word, code): + need(len(word) == 14 and all(word.count(j) == 2 for j in range(N)), + 'Need exactly two calls of each of seven sources') + parity, points = 0, [0] + for label in word: + parity ^= 1 << label + points.append(parity) + differences = {a ^ b for a in points for b in points} + return {m for m in range(1, 128) if mandatory_scan(code) >> m & 1} - differences + + +def controls(codes, witness): + code = tuple(witness['code']) + word = list(range(N)) + witness['second_order'] + missing = set(witness['missing_masks']) + need(len(missing) == 22 and missing_for_word(word, code) == missing, + 'Attaining missing-set witness') + for shift in range(14): + rotated = word[shift:] + word[:shift] + need(missing_for_word(rotated, code) == missing, 'Closed-word rotation') + for transposition in combinations(range(N), 2): + relabel = list(range(N)) + a, b = transposition + relabel[a], relabel[b] = relabel[b], relabel[a] + new_word = [relabel[j] for j in word] + new_code = tuple(sorted(sum(((h >> j) & 1) << relabel[j] for j in range(N)) + for h in code)) + need(new_code in codes, 'Code inventory closes under coordinate relabeling') + need(len(missing_for_word(new_word, new_code)) == 22, 'Relabeled witness') + # Prior star's repeated-axis code supplies a discriminating positive case. + axes = (1, 1, 1, 1, 2, 4, 8) + star_code = tuple(sorted({sum(((r & v).bit_count() % 2) << j + for j, v in enumerate(axes)) for r in range(16)})) + star_word = (0, 1, 0, 1, 4, 5, 6, 2, 3, 2, 3, 4, 5, 6) + q, points = 0, [0] + for label in star_word: + q ^= 1 << label + points.append(q) + coverage = {h & (a ^ b) for h in star_code for a in points for b in points} + need(coverage == set(range(128)) and star_code not in codes, + 'Repeated-axis positive control must remain feasible') + need(mandatory_scan(code) != UNIVERSE ^ 1, 'Not every mask is mandatory') + need(0 not in missing and 127 not in missing, 'Zero and full-mask boundaries') + need(len(missing) > 21, 'False deficit ceiling 21') + need(len(missing) < 23, 'False deficit floor 23') + for bad in (word[:-1], [word[1]] + word[1:]): + try: + missing_for_word(bad, code) + except ValueError: + continue + raise ValueError('Invalid source multiplicity accepted') + return {'cyclic_rotations': 14, 'coordinate_transpositions': 21, + 'repeated_axis_positive': 1, 'false_variant_controls': 4, + 'invalid_word_rejections': 2} + + +def source_pins(): + record = json.loads((HERE / 'SOURCES.json').read_bytes()) + checked = [] + for row in record['files']: + if row['usage'] != 'input': + continue + path = HERE.parents[1] / row['path'] + need(sha256(path.read_bytes()).hexdigest() == row['sha256'], + 'Changed cited source: ' + row['path']) + checked.append(row['path']) + need(len(checked) == 2, 'Both cited main-tree source inputs are bound') + return checked + + +def main(): + pins = source_pins() + first_codes, second_codes = axis_codes(), orthogonal_codes() + need(first_codes == second_codes and len(first_codes) == 30, + 'Two complete code-domain generators must agree') + primary = census(first_codes) + secondary = census(second_codes, secondary=True) + need(primary == secondary, 'Every missing-mask set must agree, not only minima') + values, histogram, minimum, witness = primary + need(minimum == 22 and 0 not in histogram, 'Distinct-axis exclusion') + need(histogram[22] == 4, 'All four minimum-deficit pairs') + check = controls(first_codes, witness) + encoded = b''.join(value.to_bytes(16, 'big') for value in values) + files = {path.name: sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.iterdir()) if path.is_file()} + print(json.dumps({'status': 'PASS_SEVEN_SOURCE_DISTINCT_AXIS_OBSTRUCTION', + 'claim_type': 'scoped obstruction with exhaustive finite certificate', + 'codes': len(first_codes), 'orders': 5040, 'cases': len(values), + 'mandatory_per_code': 57, 'minimum_missing_mandatory_masks': minimum, + 'maximum_nonzero_outputs_if_full_mask_served_upper_bound': 105, + 'histogram': histogram, 'attaining_deficit_witness': witness, + 'census_sha256': sha256(encoded).hexdigest(), 'controls': check, + 'source_inputs': pins, 'package_sha256': files}, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()