diff --git a/research/centre-fifteen-owner-equality/PROOF.md b/research/centre-fifteen-owner-equality/PROOF.md new file mode 100644 index 0000000000..93ff1f253d --- /dev/null +++ b/research/centre-fifteen-owner-equality/PROOF.md @@ -0,0 +1,128 @@ +# The fifteen-owner equality case + +## Statement + +Let G=(B,D,E) be a finite nonempty simple bipartite graph. Assume minimum +degree at least three, no four-cycles, |B|=15, and the following bounds on +the number c6(d) of unoriented simple six-cycles through each d in D: + + c6(d) <= 1 when deg(d)=3; + c6(d) <= floor(deg(d)^2/4) when deg(d)>=4. + +Then both parts have fifteen vertices and every vertex has degree three. +The six-cycles are vertex disjoint. Write t for their number. Either t=0, +or 2<=t<=5. In particular, an equality graph cannot have exactly one +six-cycle. + +There is also an explicit necessary matrix identity. Let C be its 15 by 15 +zero-one incidence matrix, with rows indexed by B. Let J be the all-ones +matrix. There are partial permutation matrices P and Q with exactly the +same 3t active rows and 3t active columns such that + + C C^T C = 4 C + J + P - Q. (1) + +P matches each vertex of B on a six-cycle to the opposite vertex of D on +that cycle. Q matches it to a vertex on a different six-cycle. Every active +row and column of either matrix contains exactly one 1. Furthermore + + (P-Q) C^T = C (P-Q)^T. (2) + +These are integer identities. No coefficient-field reduction is used. +When t=0, (1) reduces to C C^T C = 4 C + J. + +## 1. The new equality reduction + +We use Sagar Thakrar's local path-counting inequality from PR3291, +PROOF.md section 2, as a cited lemma: + + |B| >= 5 deg(d) - c6(d). (3) + +Its hypotheses are precisely minimum degree three and absence of four-cycles. +We do not re-audit the route extraction or the predecessor's floor proof. +For 4<=k<=15, the lower bound 5k-floor(k^2/4) takes the values + + 16,19,21,23,24,25,25,25,24,23,21,19. + +Every value exceeds 15. A simple graph with fifteen vertices in B has +no D degree greater than fifteen, so all vertices of D have degree three. + +If b in B had degree at least four, root at an adjacent d. Its three B +neighbors have at least 3+2+2=7 other D neighbors. They are distinct because +there are no four-cycles. Each has two further B neighbors. There are at +least fourteen incidences to level three. Collapsing them to distinct B +vertices can save at most c6(d)<=1 vertices, by the collision count used in +(3). These vertices are outside the three first-level vertices. This would +require |B|>=3+14-1=16. Thus every B vertex also has degree three. Counting +edges gives 3|D|=3|B|, hence |D|=15. + +This extends the predecessor's fourteen-owner contradiction to a structural +statement at its sharp equality size. It does not improve the bound fifteen. + +## 2. Six-cycles are disjoint + +Two distinct six-cycles cannot share a D vertex, by its cap. If they shared +a B vertex, each would use two of its three edges. They would therefore +share an edge and its D endpoint, also impossible. Thus all six-cycles are +vertex disjoint. The same cap of one now holds at B vertices. Each cycle +uses three vertices of each part, so t<=5. + +## 3. The signed defect + +For b in B and d in D, (C C^T C)_(b,d) counts length-three walks from b to d. +If they are adjacent, exactly five such walks exist: three backtrack at b +and three backtrack at d, with the single-edge backtrack counted twice. +A further walk would form a four-cycle. Thus the entry is five. + +If b and d are not adjacent, all these walks are simple paths. Let p_b(d) +be their number. Two different paths between these endpoints have disjoint +interiors: sharing either interior vertex would create a four-cycle. Hence + + c6(b) = sum_(d not adjacent to b) binom(p_b(d),2). (4) + +Each six-cycle through b has a unique opposite endpoint d, which proves +both directions of this counting identity. + +There are twelve length-three paths from b to nonneighbors: choose one of +three first edges, one of two second edges, and one of two third edges. +No such path can return to a neighbor, since there are no four-cycles. +There are also exactly twelve nonneighbors in D. + +If c6(b)=0, (4) forces all twelve path counts to be one. If c6(b)=1, it +forces exactly one count to be two, exactly one to be zero, and the other +ten to be one. The doubled endpoint is the opposite vertex on b's unique +six-cycle. The zero endpoint is unique. + +Apply the same argument after interchanging B and D. It shows that a +column of the defect matrix + + E = C C^T C - 4C - J + +is zero off the six-cycles; on a six-cycle it has one +1 and one -1. +The row statement is identical. Thus the positive entries form P, the +negative entries form -Q, and their active row and column sets are exactly +the vertices on the six-cycles. This proves (1) and the asserted partial +permutation structure. + +For an active b, its own six-cycle contains three D vertices. Two are +adjacent to b, while the third has two length-three paths from b. None is +the zero-path endpoint. The Q endpoint therefore lies on another cycle. +If there were exactly one six-cycle, there would be no such endpoint. +This excludes t=1. + +Finally, E C^T = (C C^T)^2 - 4 C C^T - 3J is symmetric, since every row +of C has sum three. Transposing gives (2). + +## 4. What this does and does not settle + +The six-cycle-free duad/perfect-matching graph in PR3291 attains the +hypotheses, so the equality class is nonempty. Its established floor and +classical geometry retain their credit. We do not claim uniqueness of that +graph, nor exclude equality graphs with two through five six-cycles. + +For a future route-labelled fifteen-owner search, every candidate can now +be restricted to a cubic fifteen-by-fifteen incidence with the signed defect +above. If it has a six-cycle, it must have at least two disjoint ones, and +the negative defect matches between different cycles. Actual route labels, +scalar coefficient equations and physical realization are additional +obligations. The present theorem supplies no common-kernel vector, cheaper +repair, paid profile, supplier admission or new kappa. diff --git a/research/centre-fifteen-owner-equality/README.md b/research/centre-fifteen-owner-equality/README.md new file mode 100644 index 0000000000..efd51a7863 --- /dev/null +++ b/research/centre-fifteen-owner-equality/README.md @@ -0,0 +1,110 @@ +# Cubic structure and a signed defect at fifteen owners + +**Scoped written proof with finite exact corroboration. No new kappa.** +Every graph attaining Sagar Thakrar's PR3291 fifteen-owner abstract floor is +cubic on fifteen vertices per side. Its six-cycles are vertex disjoint, and +it cannot have exactly one six-cycle. This contribution is produced by +Nick Petalas. + +The new structural identity, over the integers, is + + C C^T C = 4C + J + P - Q, + (P-Q) C^T = C (P-Q)^T. + +C is the incidence matrix. P and Q are partial permutation matrices on the +vertices lying on six-cycles. P matches opposite vertices on each cycle; +Q matches vertices on different cycles. If there are t six-cycles, their +active sets have size 3t. Thus t is either zero or one of 2,3,4,5. +[PROOF.md](PROOF.md) gives the universal argument and exact hypotheses. + +This is a new restriction on the equality search left by PR3291 and +Matarener's PR3656. Their floor, geometry, source extraction and coset +certificate are cited without replay or audit. We do not classify every +equality graph or prove that the six-cycle-free example is unique. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/centre-fifteen-owner-equality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/centre-fifteen-owner-equality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/centre-fifteen-owner-equality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/centre-fifteen-owner-equality --check-source-history +``` + +Substitute an installed CPython 3.12 path elsewhere. The direct verifier is +read-only and prints a generated receipt bound to every package file by +SHA256, followed by `PASS_CENTRE_FIFTEEN_OWNER_EQUALITY`. + +The bounded corroboration visits all 531,441 local path profiles in +{0,1,2}^12, including the 133 profiles admitted by the path-sum/cycle cap; +checks the twelve possible noncubic root degrees; and checks the integer +defect on the duad/perfect-matching graph. All 720 eligible two-edge switches +of that graph are tested. Exactly 360 are four-cycle-free and all 360 fail +the six-cycle cap. Independent intersection and literal-walk cycle counters +agree on their complete cycle sets. This is a bounded control family, not +an enumeration of all fifteen-owner graphs or evidence that the remaining +cycle counts are impossible. No nonzero-defect equality graph is supplied; +nonzero local profiles are checked independently of graph realization. + +Controls reject malformed equality boundaries and local path profiles, and +a cubic C4-free fifteen-by-fifteen cyclic graph specifically at the six-cycle +capacity gate. Literal matrix multiplication supplies a separate path-count +check. Normal and optimized commands retain every check. + +## Connection and limits + +The original `centre-path-sharing` card is changed to a structural side +question in the retained one-to-one block-repair model. The theorem assumes +the abstract minimum-degree, C4-free and cycle-cap conditions. It does not +recompute the routes or prove those conditions for another supplier. + +For a route-labelled equality search, the cubic restriction removes larger +degrees, and the P/Q identity supplies necessary equations before checking +route labels and scalar coefficients. These obligations remain open. No +physical acquisition, dirty restoration, frame conversion, hosting, precision, +stock, recursive invoice, all-size compiler, admitted supplier or complete +multiplication theorem is supplied. The selected frontier remains unchanged. +Independent human and formal proof-kernel review are unclaimed. No selected +cold replay, Lean or Docker run is part of this result. + +The historical card control fails with `KeyError: 'complex_profile'` against +the selected schema. The current `research_selected_baseline.py` binding +control passes. These are orientation observations, not scientific premises. + +The checker has no recursion, subprocesses, network or write paths. Graphs +are bounded to 32 vertices per side; actual cycle checks use cubic graphs +with fifteen vertices per side. Walks have exactly five expansion rounds. +The largest local profile domain is 3^12, processed one tuple at a time. +Functions stay below sixty physical lines. Python allocates managed objects; +fixed allocation is not claimed. These fixed domains and the registered +120-second command bounds are the compensating limits. Raw-pointer and +preprocessor rules have no direct Python counterpart. Warning-strict normal +and optimized execution and AST inspection provide diagnostics; no project +static type checker is configured for this isolated standard-library file. + +## Open next questions + +1. Can an equality graph have two through five six-cycles? Use the cubic + fifteen-by-fifteen boundary and signed partial permutations first. This + would decide whether a route search may restrict to girth eight. No such + exclusion or witness is supplied here. +2. Can a graph satisfying this stronger boundary carry the actual routes + and scalar coefficient equations? Begin with one equality incidence and + retain every route relation. The route-labelled CSP and a favorable full + physical budget remain blockers to a supplier construction. + +The structured questions are also in [TASK.json](TASK.json). + +## Credit + +Sagar Thakrar #3291 supplies the local path-counting inequality and sharp +fifteen-owner theorem. Matarener #3656 supplies the coset construction and +minimum-support question. Retain dcharb78 #3147, Ross Richardson #3071, +Gonzalo Mier #3097, Sudarsh Chaturvedi #3168, Aaron Wang/navinor, ywz65 and +the selected source lineage for the block-repair model and route conditions. +The duad/perfect-matching geometry and ordinary graph path counting are +classical; no literature-priority claim is made for them. Only the equality +reduction, signed defect and its consequences are new in this package. +Predecessor files and notices remain unchanged. Apache-2.0. diff --git a/research/centre-fifteen-owner-equality/SOURCES.json b/research/centre-fifteen-owner-equality/SOURCES.json new file mode 100644 index 0000000000..abd973070a --- /dev/null +++ b/research/centre-fifteen-owner-equality/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/centre-block-moore-bound/PROOF.md", + "usage": "provenance", + "git_blob": "57e4adae5ab6247d7f82fefc2d91abccdb4bd39a", + "sha256": "4ff55b8d7c32f4ad2e32e267fd3e3340003b580dfa709577016eb605f157e137" + }, + { + "path": "research/centre-block-moore-bound/README.md", + "usage": "provenance", + "git_blob": "82b2b72beaa1878dd933cf95a47ade8b2a0af643", + "sha256": "bbdf8be190f21ddffacc7babd79b1111e7948e4dfc37d7496bc199dd63d4d03c" + }, + { + "path": "research/centre-block-coset-kernel/README.md", + "usage": "provenance", + "git_blob": "f27dc04894b04dfbe60152adb77ac69b5b5f0628", + "sha256": "c7594aa840999aa366d834500f0b13cd870c215b321eacdfb0da43bc35d7eef6" + } + ] +} diff --git a/research/centre-fifteen-owner-equality/TASK.json b/research/centre-fifteen-owner-equality/TASK.json new file mode 100644 index 0000000000..d8a31b213e --- /dev/null +++ b/research/centre-fifteen-owner-equality/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "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": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "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": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Cubic structure and signed partial-permutation defect of the abstract fifteen-owner equality case; exact exclusion of one six-cycle.", + "scope_change_reason": "A structural side question before the route-labelled equality search, rather than a new centre supplier or a replay of predecessor claims.", + "bottleneck_link": "The necessary equality structure restricts candidates for the smallest common-kernel support before expensive route and coefficient searches; no physical cost improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved equality restriction; leave the remaining six-cycle counts and physical route realization open.", + "outcome": "completed", + "evidence": "PROOF.md; generated read-only verifier receipt; 531441 local profiles, 720 edge switches, independent cycle sets and literal integer products.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an equality graph have two through five six-cycles?", + "why_it_matters": "Decides whether girth eight is a valid restriction on the equality search.", + "first_step": "Apply the cubic boundary, signed partial permutations and defect symmetry before graph construction.", + "blocked_by": "No complete equality classification or nonzero-defect graph is supplied." + }, + { + "question": "Can an equality graph carry the actual route labels and scalar coefficient equations?", + "why_it_matters": "Determines whether the abstract equality size is attainable in the retained observation model.", + "first_step": "Bind one equality incidence to the literal routes and all scalar equations.", + "blocked_by": "Route-labelled CSP and full physical budget remain open." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit" + } +} diff --git a/research/centre-fifteen-owner-equality/VERIFY.json b/research/centre-fifteen-owner-equality/VERIFY.json new file mode 100644 index 0000000000..38b37ed96f --- /dev/null +++ b/research/centre-fifteen-owner-equality/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact local path profiles, integer defect, independent cycle sets and boundary controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete corroboration with optimization enabled." + } + ] +} diff --git a/research/centre-fifteen-owner-equality/verify.py b/research/centre-fifteen-owner-equality/verify.py new file mode 100644 index 0000000000..5c4cfb46d5 --- /dev/null +++ b/research/centre-fifteen-owner-equality/verify.py @@ -0,0 +1,247 @@ +"""Bounded exact corroboration of the fifteen-owner equality theorem.""" +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path +import sys + +MAX_SIDE = 32 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def validate(rows: tuple[int, ...], columns: int) -> tuple[int, ...]: + require(type(columns) is int and 1 <= columns <= MAX_SIDE, 'column bound') + require(1 <= len(rows) <= MAX_SIDE, 'row bound') + require(all(type(r) is int and 0 <= r < 1 << columns for r in rows), + 'invalid row') + return tuple(sum(1 << i for i, r in enumerate(rows) if r >> j & 1) + for j in range(columns)) + + +def four_free(rows: tuple[int, ...]) -> bool: + return all((a & b).bit_count() <= 1 + for a, b in itertools.combinations(rows, 2)) + + +def cycles_by_intersections(rows: tuple[int, ...]) -> set[tuple[int, ...]]: + require(four_free(rows), 'four-cycle present') + cycles = set() + for a, b, c in itertools.combinations(range(len(rows)), 3): + x, y, z = rows[a] & rows[b], rows[b] & rows[c], rows[c] & rows[a] + if x and y and z and len({x, y, z}) == 3: + edges = tuple(sorted((a * MAX_SIDE + x.bit_length() - 1, + b * MAX_SIDE + x.bit_length() - 1, + b * MAX_SIDE + y.bit_length() - 1, + c * MAX_SIDE + y.bit_length() - 1, + c * MAX_SIDE + z.bit_length() - 1, + a * MAX_SIDE + z.bit_length() - 1))) + cycles.add(edges) + return cycles + + +def cycles_by_walks(rows: tuple[int, ...], columns: int) -> set[tuple[int, ...]]: + cols = validate(rows, columns) + require(all(r.bit_count() <= 3 for r in rows + cols), 'walk degree bound') + size = len(rows) + adjacency = [tuple(size + j for j in range(columns) if r >> j & 1) + for r in rows] + adjacency += [tuple(i for i in range(size) if r >> i & 1) for r in cols] + cycles = set() + for root in range(size): + paths = [(root,)] + for _ in range(5): + paths = [path + (v,) for path in paths + for v in adjacency[path[-1]] if v not in path] + for path in paths: + if root not in adjacency[path[-1]]: + continue + edges = [] + for a, b in zip(path, path[1:] + (root,)): + if a >= size: + a, b = b, a + edges.append(a * MAX_SIDE + b - size) + cycles.add(tuple(sorted(edges))) + return cycles + + +def incidence_product(rows: tuple[int, ...], columns: int) -> list[list[int]]: + # Literal matrix product, separate from the path/edge-set enumerators. + common = [[sum((a >> j & 1) * (b >> j & 1) for j in range(columns)) + for b in rows] for a in rows] + return [[sum(common[i][k] * (rows[k] >> j & 1) + for k in range(len(rows))) for j in range(columns)] + for i in range(len(rows))] + + +def cycle_counts(cycles: set[tuple[int, ...]], size: int) -> tuple[list[int], list[int]]: + left, right = [0] * size, [0] * size + for cycle in cycles: + for i in {e // MAX_SIDE for e in cycle}: + left[i] += 1 + for j in {e % MAX_SIDE for e in cycle}: + right[j] += 1 + return left, right + + +def check_defect(rows: tuple[int, ...]) -> dict[str, int]: + cols = validate(rows, 15) + require(len(rows) == 15 and all(r.bit_count() == 3 for r in rows + cols), + 'cubic fifteen-by-fifteen boundary') + cycles = cycles_by_intersections(rows) + require(cycles == cycles_by_walks(rows, 15), 'independent cycle disagreement') + left, right = cycle_counts(cycles, 15) + require(max(left + right) <= 1, 'six-cycle capacity exceeded') + product = incidence_product(rows, 15) + defect = [[product[i][j] - 4 * (rows[i] >> j & 1) - 1 + for j in range(15)] for i in range(15)] + for i in range(15): + require(sorted(x for x in defect[i] if x) == [-1, 1] * left[i], + 'row defect') + for j in range(15): + require(sorted(defect[i][j] for i in range(15) if defect[i][j]) + == [-1, 1] * right[j], 'column defect') + for cycle in cycles: + bset = {e // MAX_SIDE for e in cycle} + dset = {e % MAX_SIDE for e in cycle} + for i in bset: + positive = [j for j in dset if not (rows[i] >> j & 1)] + require(len(positive) == 1 and defect[i][positive[0]] == 1, + 'opposite endpoint') + require(all(defect[i][j] != -1 for j in dset), 'negative same-cycle') + require(len(cycles) != 1, 'single six-cycle equality impossible') + for i in range(15): + for j in range(15): + lhs = sum(defect[i][k] * (rows[j] >> k & 1) for k in range(15)) + rhs = sum((rows[i] >> k & 1) * defect[j][k] for k in range(15)) + require(lhs == rhs, 'defect symmetry') + return {'six_cycles': len(cycles), 'active_vertices_per_part': sum(left)} + + +def doily() -> tuple[int, ...]: + duads = list(itertools.combinations(range(6), 2)) + matchings = [t for t in itertools.combinations(range(15), 3) + if len({x for i in t for x in duads[i]}) == 6] + require(len(matchings) == 15, 'matching construction') + return tuple(sum(1 << j for j, block in enumerate(matchings) if i in block) + for i in range(15)) + + +def path_profile(profile: tuple[int, ...]) -> list[int]: + require(len(profile) == 12, 'twelve nonneighbors required') + require(all(type(p) is int and 0 <= p <= 12 for p in profile), + 'invalid path count') + require(sum(profile) == 12, 'twelve paths required') + require(sum(p * (p - 1) // 2 for p in profile) <= 1, 'local cycle capacity') + return sorted(p - 1 for p in profile if p != 1) + + +def profile_checks() -> dict[str, int]: + accepted = 0 + doubled = 0 + for profile in itertools.product(range(3), repeat=12): + if sum(profile) != 12 or sum(p == 2 for p in profile) > 1: + continue + excess = sum(p * (p - 1) // 2 for p in profile) + values = path_profile(profile) + require(values == ([-1, 1] if excess else []), 'local path defect') + accepted += 1 + doubled += excess + require((accepted, doubled) == (133, 132), 'local profile completeness') + # A count >=3 would already give at least three six-cycles. + require(all(p * (p - 1) // 2 > 1 for p in range(3, 13)), 'large count') + bounds = [5 * k - k * k // 4 for k in range(4, 16)] + require(min(bounds) == 16, 'noncubic degree exclusion') + return {'profiles_visited': 3 ** 12, 'admitted_profiles': accepted, + 'nonzero_profiles': doubled, 'degree_cases': len(bounds)} + + +def switching_checks(base: tuple[int, ...]) -> dict[str, int | str]: + edges = [(i, j) for i, r in enumerate(base) for j in range(15) if r >> j & 1] + counts = {'switches': 0, 'four_free': 0, 'capacity_rejected': 0} + digest = hashlib.sha256() + for (a, x), (b, y) in itertools.combinations(edges, 2): + if a == b or x == y or base[a] >> y & 1 or base[b] >> x & 1: + continue + rows = list(base) + rows[a] ^= (1 << x) | (1 << y) + rows[b] ^= (1 << x) | (1 << y) + counts['switches'] += 1 + trial = tuple(rows) + if not four_free(trial): + continue + counts['four_free'] += 1 + cycles = cycles_by_intersections(trial) + require(cycles == cycles_by_walks(trial, 15), 'switched cycle mismatch') + left, right = cycle_counts(cycles, 15) + if max(left + right) > 1: + counts['capacity_rejected'] += 1 + else: + check_defect(trial) + digest.update(json.dumps(sorted(cycles), separators=(',', ':')).encode()) + require(counts['switches'] == 720, 'switch-domain enumeration') + counts['cycle_digest'] = digest.hexdigest() + return counts + + +def controls(base: tuple[int, ...]) -> int: + rejected = 0 + fixtures = [(base[:-1], 15), (base, 14), (base + (True,), 15), + (base + (-1,), 15)] + for rows, columns in fixtures: + try: + cols = validate(rows, columns) + require(len(rows) == 15 and all(r.bit_count() == 3 for r in rows + cols), + 'wrong equality boundary') + except ValueError: + rejected += 1 + require(rejected == len(fixtures), 'invalid boundary accepted') + # This cubic fifteen-by-fifteen graph is C4-free but violates the cycle cap. + cyclic = tuple(sum(1 << ((i + shift) % 15) for shift in (0, 1, 3)) + for i in range(15)) + require(four_free(cyclic), 'cyclic capacity control must be C4-free') + try: + check_defect(cyclic) + except ValueError as error: + require(str(error) == 'six-cycle capacity exceeded', 'wrong control cause') + rejected += 1 + else: + raise ValueError('capacity violation accepted') + malformed_profiles = [(2,) + (1,) * 11, (2, 2, 0, 0) + (1,) * 8, + (True,) + (1,) * 11, (1,) * 11] + for profile in malformed_profiles: + try: + path_profile(profile) + except ValueError: + rejected += 1 + else: + raise ValueError('malformed path profile accepted') + return rejected + + +def main() -> None: + require(len(sys.argv) == 1, 'this verifier accepts no arguments') + base = doily() + result = {'scope': 'scoped equality proof; finite corroboration only', + 'doily': check_defect(base), 'local_profiles': profile_checks(), + 'switching': switching_checks(base), 'controls': controls(base)} + root = Path(__file__).resolve().parent + names = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'verify.py') + hashes = {} + for name in names: + path = root / name + require(path.stat().st_size <= 262144, 'package file bound') + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + result['source_sha256'] = hashes + print(json.dumps(result, sort_keys=True)) + print('PASS_CENTRE_FIFTEEN_OWNER_EQUALITY') + + +if __name__ == '__main__': + main()