diff --git a/research/p104-coordinate-symmetry/PROOF.md b/research/p104-coordinate-symmetry/PROOF.md new file mode 100644 index 0000000000..9f98ea00b1 --- /dev/null +++ b/research/p104-coordinate-symmetry/PROOF.md @@ -0,0 +1,117 @@ +# Exact coordinate symmetry and its frame quotient + +This is a source-specific finite group certificate followed by a scoped +counting proof. All vector spaces in this note are over F2. No physical +supplier theorem follows from these statements. + +## The coordinate group + +Let P be the set of 104 nine-bit integers in the pinned `ports.json`. +A coordinate permutation sends bit i to bit pi(i), with zero-based indices. +Let G consist of the permutations pi in S9 for which pi(P)=P. + +**Finite certificate.** G has exactly two elements. Its nonidentity element is + + sigma = (0 3)(2 8)(4 7)(5 6), + +and coordinate 1 is fixed. In image-list notation this is +`[3,1,8,0,7,6,5,4,2]`. + +Here is the complete finite reduction used by the checker. Every member of P +has weight three or seven. Among all weight-three masks the missing masks are + + 7,25,42,52,67,76,82,97,104,137,162,266,289,448. + +Among all weight-seven masks the missing masks are `127,491`. A coordinate +permutation preserves weight. It preserves P if and only if it preserves both +of these missing sets. The checker visits every one of the 9! permutations. +Exactly 960 preserve the weight-seven missing set, and exactly identity and +sigma also preserve the weight-three missing set. For each survivor it also +checks the image of every original port. This is an exhaustive certificate, +not a computer-free proof of the two-survivor step. + +The 960 count also has a direct check. The complements of the two missing +weight-seven masks have supports `{7,8}` and `{2,4}`. Their setwise stabilizer +has size `2! * 2! * 2! * 5! = 960`. The first two factors exchange the ends of +the two pairs, the third exchanges the pairs, and the last permutes the other +five coordinates. + +The induced port action has eight fixed ports + + 11,98,146,251,262,367,415,502, + +and 48 two-element orbits. Hence the exact port quotient has 56 elements. +These are binary coordinate symmetries of this literal label set. They are +not the full root-system symmetry group or the full binary linear stabilizer. + +## Invariant frames of an involution + +The following elementary counting argument is included to state exactly what +the finite computation implies for every frame dimension. Gaussian binomial +coefficients and the orbit-counting lemma are classical; the contribution is +the exact application to this pinned P104 coordinate action. + +Let V have dimension n, let N:V->V satisfy N^2=0, and put +`a=rank N`, `h=n-a`. Write `[b choose c]_2` for the number of c-dimensional +subspaces of F2^b, and zero when c is outside `0..b`. The number of +k-dimensional subspaces U with N(U) contained in U is + + f(n,a,k) = sum_r [a choose r]_2 [h-r choose k-2r]_2 + * 2^(r*(h-k+r)), (1) + +where the sum includes just `0<=r<=min(a,floor(k/2))` and `k-r<=h`. + +To prove (1), set `R=N(U)` and `S=U intersect ker N`, so `dim R=r` and +`dim S=k-r`. Invariance is exactly the additional inclusion R contained in S. +First choose R inside im N, in `[a choose r]_2` ways. Since im N is contained +in ker N, choose S containing R inside the h-dimensional ker N, in +`[h-r choose k-2r]_2` ways. + +For a fixed R,S, the map from `N^-1(R)/S` to R induced by N is onto, with +kernel `ker N/S` of dimension `h-k+r`. Each admissible U/S is the image of a +linear section of this map, and every section gives an admissible U. A fixed +section identifies the remaining sections with +`Hom(R,ker N/S)`, which has `2^(r*(h-k+r))` elements. A section is uniquely +determined by its image because N restricts to its inverse there. This also +proves there is no overcount. Multiplying and summing proves (1). + +For sigma above, put N=sigma+I. Each of the four exchanged coordinate pairs +contributes one rank to N, and the fixed coordinate contributes zero. Thus +N^2=0, a=4 and h=5. A frame is sigma-invariant exactly when it is N-invariant. +Formula (1) gives the fixed-frame profile, in dimensions zero through nine, + + 1,31,395,1955,4371,4371,1955,395,31,1. (2) + +Every frame that is not fixed has a two-element orbit. Consequently the exact +number of coordinate-symmetry orbits on k-frames is + + ([9 choose k]_2 + f(9,4,k)) / 2. (3) + +The checker independently enumerates every reduced binary basis in every +one of these ten Grassmannians, tests sigma-invariance directly and compares +the resulting counts to (1). The proof of (1) does not depend on this census. + +For planes, `[9 choose 2]_2=43435` and `f(9,4,2)=395`, so (3) is **21915**. +The 395 fixed planes split as 155 planes contained in ker N and 240 planes +with rank-one N restriction. This split also follows immediately from (1). + +## What the result excludes, and what it permits + +Any quotient based only on coordinate permutations preserving all literal +ports has equivalence classes of size at most two. A more constrained caller +or frozen word may have fewer symmetries. For the pure plane search, the +exact reduction is 43435 candidates to 21915 representatives. This is a count +of equivalence classes, not a wall-time guarantee or a proof that a particular +caller permits the nonidentity relabeling. + +Global invariance does allow proper frames. For example, the line generated +by port 11 is fixed, and the plane spanned by masks 1 and 8 is fixed while +neither generating line is fixed. The symmetry hypothesis alone therefore +cannot force a shared frame to have dimension nine. Equation (2) gives its +precise finite admissible-space counts. It does not decide productive target +capacity, chronology, physical delivery or restoration on any of those spaces. + +Larger binary linear maps, signed root maps in another coordinate system, +multiple frames permuted by a group, changed port sets and nonsymmetric words +are outside the coordinate-permutation contract. The result is not an +obstruction to those routes or a universal bound on P104 helper constructions. diff --git a/research/p104-coordinate-symmetry/README.md b/research/p104-coordinate-symmetry/README.md new file mode 100644 index 0000000000..c60168098f --- /dev/null +++ b/research/p104-coordinate-symmetry/README.md @@ -0,0 +1,134 @@ +# Exact P104 coordinate symmetry + +**Finite certificate with a scoped counting proof. No new kappa.** +This contribution was produced by Nick Petalas. + +The literal 104-port set has exactly two coordinate-permutation symmetries. +In zero-based coordinates the nonidentity symmetry is + + (0 3)(2 8)(4 7)(5 6), + +with coordinate 1 fixed. Thus a search quotient using only coordinate +permutations preserving all ports has classes of size at most two. On the +43,435 binary planes in F2^9, the exact quotient has **21,915** elements. +This gives a sharp limit on that search-reduction method, rather than a +physical supplier or a claim about every symmetry of P104. + +There are exactly 395 invariant planes. More generally, the invariant-frame +counts in dimensions zero through nine are + + 1,31,395,1955,4371,4371,1955,395,31,1. + +[PROOF.md](PROOF.md) gives an elementary section-counting formula for +square-zero linear maps and applies it to this involution. Gaussian subspace +counting and orbit counting are classical. The new result is the exact +coordinate group and its source-specific frame quotient. No general +mathematical priority is claimed for the counting tools. + +The symmetry requirement permits proper shared frames. The line generated +by port 11 is fixed. The plane generated by masks 1 and 8 is fixed although +its two generating lines are exchanged. Symmetry alone therefore supplies +no full-dimension lower bound. A particular caller must still establish +productive capacity, chronological delivery and complete charges. + +## Reproduce + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/p104-coordinate-symmetry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/p104-coordinate-symmetry/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-coordinate-symmetry +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-coordinate-symmetry --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter prefix. +The direct verifier prints `PASS_P104_COORDINATE_SYMMETRY` in a generated +JSON receipt with zero errors, interpreter version and source/package hashes. +It writes no files and imports no predecessor code. + +The checker visits all 362,880 coordinate permutations. Its weight-seven +filter leaves 960 candidates, and the weight-three filter leaves two. +It independently enumerates all 8,283,458 reduced binary frames across all +ten dimensions and tests invariance directly. The plane count is 43,435, +and exactly 395 are fixed. Sixteen small Jordan-type domains independently +check the counting formula on 12,668 frames. Seven rejection controls and +seven semantic controls include corrupt input bytes, invalid frame domains, +a false port symmetry, a moving line and an invariant plane with moving +lines. All conditions use exceptions and remain active under `-O`. + +[SOURCES.json](SOURCES.json) pins the exact input, source base, original card +and selected record. The external port file is declared in [VERIFY.json](VERIFY.json) +for replay selection and export. The catalogue and selected record are +historical provenance. The finite coordinate-group certificate and the +written counting proof are different evidence types; the census corroborates +the latter and does not replace mathematical review. + +## Scope and relevance + +The coverage-law card is explicitly changed to a computational geometry side +result for the current helper-interface bottleneck. The source-binding first +example passes, and the selected record resolves to conditional kappa +`781451/250000000 = 0.003125804`. No selected file is changed. + +The factor-two cap applies only to binary coordinate permutations preserving +the literal port set. Larger binary linear stabilizers, signed root actions +in other coordinates, changed label sets, and several frames permuted among +themselves are outside the result. A frozen scalar word or caller may admit +only the identity. The orbit counts do not assert a wall-time saving. + +No predecessor theorem, invoice or numerical result is audited. No paid word, +helper restoration, native realization, precision/tape layout, stock, +compiler, supplier admission or complete multiplication theorem is supplied. +The selected cold replay, Lean, Docker, independent human review and formal +proof-kernel review are unrun. All five selected framework assumptions remain. + +Live handoffs, active Discussions, open/account PRs, local reservations and +main/merged term searches were checked before reservation and publication. +The cached overlap search covered 338 open PRs and 5,947 Discussion records, +but only 87 of 8,623 local notes. Direct Git searches of main README contents +supplemented that sparse coverage. This does not prove global novelty. + +## Open next questions + +Can non-coordinate binary linear symmetries give a larger useful quotient? +Start by computing the full GL9(F2) stabilizer from the port incidence structure, +then intersect it with the actual scalar/native caller constraints. A port-set +symmetry alone is not a legal source-word relabeling, and brute force over all +invertible matrices is not a proposed search method. + +Can one of the proper invariant frames support a fully charged helper +interface? Start with one explicit frame and one causal cut, then prove +independent input/output delivery, restoration and the complete signed bill. +The present finite frame counts establish none of those obligations. +Structured questions are in [TASK.json](TASK.json). + +## Verification design + +Build the Lever led to a deterministic checker that covers the whole finite +domain. Prove It Works led to a separate literal invariance census rather +than accepting the counting formula alone. The Power of Ten inspection keeps +all functions below sixty lines, uses no recursion, dynamic code generation, +subprocesses or external solvers, and enforces n<=9. Every RREF assignment has +at most twenty binary parameters. Only one basis is retained during the full +frame census, and the coordinate-group list has two entries. + +CPython integers, tuples and generators allocate during execution. This is a +managed-runtime deviation from allocation-free steady operation. The enforced +finite input domain bounds live state; no census-sized set is stored. The +receipt hashes at most the six explicit package files and the one bounded +source file. Warning-strict normal and optimized execution supply local +interpreted-code diagnostics. This is an exact finite verifier, not a physical +fixed-storage implementation. + +## Credit + +Matarener's [PR6166](https://github.com/CrocSwap/integer-mult-bounds/pull/6166) +supplies the retained literal port list and its E8 interpretation. +Ali Romman's PR5827 and DreamingOfClouds's PR5907/PR6030 supply the local-word +lineage credited by that source. DreamingOfClouds's A2-family work supplies +related signed root symmetries, which are a different action from binary +coordinate permutations. The retained decoder, native, compiler and outer +contributors keep their attribution. Their scientific results are cited +context, not rechecked deliverables. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/p104-coordinate-symmetry/SOURCES.json b/research/p104-coordinate-symmetry/SOURCES.json new file mode 100644 index 0000000000..f10e0ed3cb --- /dev/null +++ b/research/p104-coordinate-symmetry/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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/p104-carrier-code-uniqueness/e8/ports.json", + "usage": "input", + "git_blob": "b964c3ae2ea54d3763d74639d691ea9f5b02920e", + "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" + } + ] +} diff --git a/research/p104-coordinate-symmetry/TASK.json b/research/p104-coordinate-symmetry/TASK.json new file mode 100644 index 0000000000..09da364bcd --- /dev/null +++ b/research/p104-coordinate-symmetry/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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" + ], + "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 source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "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": "Determine the exact coordinate-permutation stabilizer of the literal P104 port set and its invariant-frame and Grassmannian-orbit counts.", + "scope_change_reason": "A new symmetry-constrained frame-search side result replaces construction of a complete changed productive-credit interface. It does not meet supplier admission or claim a changed invoice.", + "bottleneck_link": "Side result: bounds coordinate-symmetry compression when exploring new shared helper frames at the binding complex interface.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact useful restriction; stop at the coordinate group and its invariant-frame census without extending to general linear or native symmetries.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py: all 362880 permutations, all 8283458 binary frames, 16 small Jordan domains and 14 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can non-coordinate binary linear symmetries give a larger useful quotient?", + "why_it_matters": "The coordinate-only quotient has classes of size at most two.", + "first_step": "Recover the full binary linear port stabilizer from incidence, then intersect it with one actual caller contract.", + "blocked_by": "Port incidence symmetries need not preserve the fixed word or native endpoints." + }, + { + "question": "Can a proper invariant frame support a fully charged helper interface?", + "why_it_matters": "The exact census admits many proper frames but establishes no productive-credit gain.", + "first_step": "Choose one explicit frame and causal cut, and derive independent input/output delivery, restoration and a complete signed invoice.", + "blocked_by": "Chronology, native delivery and complete costs remain unproved." + } + ] +} diff --git a/research/p104-coordinate-symmetry/VERIFY.json b/research/p104-coordinate-symmetry/VERIFY.json new file mode 100644 index 0000000000..1823ffd041 --- /dev/null +++ b/research/p104-coordinate-symmetry/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-carrier-code-uniqueness/e8/ports.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact coordinate group, full all-dimension invariant-frame census, counting formula, source binding and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact coordinate group, full all-dimension invariant-frame census, counting formula, source binding and rejecting controls." + } + ] +} diff --git a/research/p104-coordinate-symmetry/verify.py b/research/p104-coordinate-symmetry/verify.py new file mode 100644 index 0000000000..b12a5e5f1d --- /dev/null +++ b/research/p104-coordinate-symmetry/verify.py @@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +"""Exact coordinate stabilizer and invariant-frame census. Apache-2.0.""" +import hashlib +import itertools +import json +import math +import platform +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +SOURCE = "research/p104-carrier-code-uniqueness/e8/ports.json" +FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +SOURCE_HASH = "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" +SIGMA = (3, 1, 8, 0, 7, 6, 5, 4, 2) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_ports(data): + require(hashlib.sha256(data).hexdigest() == SOURCE_HASH, "source hash") + ports = json.loads(data) + require(isinstance(ports, list) and len(ports) == 104, "port list length") + require(all(type(x) is int and 0 < x < 512 for x in ports), "port domain") + require(len(set(ports)) == 104, "distinct ports") + require({x.bit_count() for x in ports} == {3, 7}, "weight classes") + return frozenset(ports) + + +def act(value, permutation): + return sum(((value >> i) & 1) << permutation[i] for i in range(len(permutation))) + + +def coordinate_stabilizer(ports): + missing = {w: frozenset(x for x in range(512) + if x.bit_count() == w and x not in ports) for w in (3, 7)} + require(len(missing[3]) == 14 and len(missing[7]) == 2, "complement sizes") + group = [] + candidates = 0 + visited = 0 + for permutation in itertools.permutations(range(9)): + visited += 1 + if frozenset(act(x, permutation) for x in missing[7]) != missing[7]: + continue + candidates += 1 + if frozenset(act(x, permutation) for x in missing[3]) == missing[3]: + require(frozenset(act(x, permutation) for x in ports) == ports, + "full port preservation") + group.append(permutation) + require(visited == math.factorial(9), "permutation coverage") + require(candidates == 960, "weight-seven filter count") + require(group == [tuple(range(9)), SIGMA], "exact stabilizer") + return group, visited, candidates + + +def subspaces(n, k): + """Unique reduced bases with least-set-bit pivots, including the zero space.""" + require(type(n) is int and 0 <= n <= 9, "ambient dimension") + require(type(k) is int and 0 <= k <= n, "frame dimension") + for pivots in itertools.combinations(range(n), k): + free = tuple((i, j) for i, p in enumerate(pivots) + for j in range(p + 1, n) if j not in pivots) + require(len(free) <= 20, "RREF parameter bound") + for bits in range(1 << len(free)): + rows = [1 << p for p in pivots] + for index, (i, j) in enumerate(free): + rows[i] |= ((bits >> index) & 1) << j + yield tuple(rows) + + +def contains(basis, value): + for row in basis: + if value & (row & -row): + value ^= row + return value == 0 + + +def invariant(basis, action): + return all(contains(basis, action[row]) for row in basis) + + +def gaussian(n, k): + require(type(n) is int and 0 <= n <= 9, "Gaussian ambient dimension") + if k < 0 or k > n: + return 0 + numerator = math.prod((1 << (n - j)) - 1 for j in range(k)) + denominator = math.prod((1 << (k - j)) - 1 for j in range(k)) + require(numerator % denominator == 0, "Gaussian integrality") + return numerator // denominator + + +def fixed_formula(n, rank, k): + require(0 <= rank <= n // 2 and 0 <= k <= n <= 9, "nilpotent domain") + h = n - rank + total = 0 + for image_dim in range(min(rank, k // 2) + 1): + kernel_dim = k - image_dim + if kernel_dim <= h: + total += (gaussian(rank, image_dim) + * gaussian(h - image_dim, k - 2 * image_dim) + * (1 << (image_dim * (h - kernel_dim)))) + return total + + +def census(n, action): + require(len(action) == 1 << n and action[0] == 0, "linear-action domain") + totals = [] + fixed = [] + for k in range(n + 1): + count = stationary = 0 + for basis in subspaces(n, k): + count += 1 + stationary += invariant(basis, action) + require(count == gaussian(n, k), "RREF census completeness") + totals.append(count) + fixed.append(stationary) + return totals, fixed + + +def small_controls(): + domains = checked = 0 + for n in range(7): + for rank in range(n // 2 + 1): + permutation = list(range(n)) + for i in range(rank): + permutation[2 * i], permutation[2 * i + 1] = 2 * i + 1, 2 * i + action = tuple(act(x, permutation) for x in range(1 << n)) + totals, fixed = census(n, action) + require(fixed == [fixed_formula(n, rank, k) for k in range(n + 1)], + "small Jordan-type formula control") + domains += 1 + checked += sum(totals) + return domains, checked + + +def port_orbits(ports, action): + orbits = {tuple(sorted({x, action[x]})) for x in ports} + require(set().union(*(set(o) for o in orbits)) == ports, "port orbit coverage") + require(sum(map(len, orbits)) == len(ports), "disjoint port orbits") + sizes = {str(k): sum(len(o) == k for o in orbits) for k in (1, 2)} + require(sizes == {"1": 8, "2": 48}, "port orbit profile") + return {"count": len(orbits), "sizes": sizes, + "fixed_labels": sorted(x for x in ports if action[x] == x)} + + +def rejection_controls(data, ports, action): + rejected = 0 + for bad in (data + b" ", data.replace(b"11", b"12", 1)): + try: + read_ports(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("corrupt source accepted") + for n, k in ((10, 1), (9, 10), (-1, 0), (3, -1), (True, 0)): + try: + next(subspaces(n, k)) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid Grassmannian accepted") + wrong = (1, 0, 2, 3, 4, 5, 6, 7, 8) + require({act(x, wrong) for x in ports} != ports, "false port symmetry rejected") + require(not invariant((1,), action), "moving line is not invariant") + require(invariant((1, 8), action), "moving-line orbit plane is invariant") + require(invariant((11,), action), "fixed-port line is invariant") + require(sum(action[x] == x for x in range(512)) == 32, "fixed vector count") + require(len({action[x] ^ x for x in range(512)}) == 16, "nilpotent rank") + require(all(action[action[x]] == x for x in range(512)), "involution") + return {"rejections": rejected, "semantic_controls": 7} + + +def main(): + data = (PACKAGE.parents[1] / SOURCE).read_bytes() + ports = read_ports(data) + group, visited, candidates = coordinate_stabilizer(ports) + action = tuple(act(x, SIGMA) for x in range(512)) + controls = rejection_controls(data, ports, action) + totals, fixed = census(9, action) + predicted = [fixed_formula(9, 4, k) for k in range(10)] + require(fixed == predicted, "all-dimension fixed-frame formula") + require(fixed == [1, 31, 395, 1955, 4371, 4371, 1955, 395, 31, 1], + "source fixed-frame profile") + orbit_counts = [(a + b) // 2 for a, b in zip(totals, fixed)] + require(all((a + b) % 2 == 0 for a, b in zip(totals, fixed)), "Burnside integrality") + require(orbit_counts[2] == 21915 and totals[2] == 43435, "plane quotient") + small_domains, small_frames = small_controls() + result = { + "status": "PASS_P104_COORDINATE_SYMMETRY", "errors": 0, + "claim_type": "finite certificate and scoped counting proof", "new_kappa": False, + "permutations_checked": visited, "weight_seven_candidates": candidates, + "group": group, "port_orbits": port_orbits(ports, action), + "frame_counts_by_dimension": totals, "fixed_frames_by_dimension": fixed, + "frame_orbits_by_dimension": orbit_counts, "frames_enumerated": sum(totals), + "small_jordan_domains": small_domains, "small_frames_enumerated": small_frames, + "controls": controls, "python": platform.python_version(), + "source_sha256": hashlib.sha256(data).hexdigest(), + "package_sha256": {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in FILES}, + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()