diff --git a/research/centre-two-coset-separation/PROOF.md b/research/centre-two-coset-separation/PROOF.md new file mode 100644 index 0000000000..0b542dae6f --- /dev/null +++ b/research/centre-two-coset-separation/PROOF.md @@ -0,0 +1,148 @@ +# Two left cosets cannot create an additional centre-kernel direction + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof, with a source-bound finite premise and +small exact corroboration. Independent human and formal proof-kernel review +are unclaimed. The theorem is about the historical scalar observation +contract of PR3071/3291/3656/3797/3828, not the current P104 native word. + +## 1. Contract and inherited premises + +Let G act regularly on its owner labels, let H be a finite subgroup, and let +rho_p be involutions indexed by ports p. Work over Q or C. R_p is a column +of a fixed reader R. For inputs supported on B, retain every later output, +including outputs outside B, and put + +```text +Sx(g) = sum_p R_p x(g,p), +4Tx(z) = sum_p R_p x(z rho_p,p). +``` + +For D={a,b,c}, suppose the following conditions hold. + +1. The right-coset partition of the ports by H rho_p consists of D and + singleton classes. H is generated by rho_a rho_b and rho_a rho_c. +2. R_D has rank two with kernel generated by u=(1,-1,-1). +3. Every pair of distinct reader columns is linearly independent. +4. For W=span(R_a,R_b), every R_p with p outside D is outside W. + +The single-block coset classification, subgroup order 4080, reader rank +eight, and one constant triple direction per left translate are **cited +premises**, from Clear1nsight's PR3828 and Ross Richardson's PR3797. +Sagar Thakrar's PR3291, through PR3071's source reader, supplies the +nonparallel-column premise. These predecessor results are not audited here. +Matarener's PR3656 supplies the original subgroup and constant witness. + +Condition 4 is the additional source check. On the authenticated reader, +exact elimination gives rank(R_0,R_6,R_p)=3 for each of the 109 ports outside +{0,6,85}, and rank two for those three ports. The program extracts R from +the archived canonical prefix using the retained query convention. It does +not execute a predecessor verifier or repeat the group/coset census. + +## 2. Separation lemma + +Let B_1=sH and B_2=tH be distinct left cosets. They are disjoint. At any +fixed later output z, the ports arriving from B_i are either absent, one +singleton port, or exactly D. This follows from the right-coset partition +after left translation by s or t. + +There are two additional exclusions. + +* If both blocks contribute singleton ports p and q, then p differs from q. + Indeed, B_1 rho_p and B_2 rho_p are disjoint, since right multiplication + by rho_p is a bijection. +* Both blocks cannot contribute D at the same z. Their triple output sets + are B_1 rho_a and B_2 rho_a, which are disjoint by the same bijection. + +Now impose Tx(z)=0. If only a singleton arrives, its coefficient is zero. +For two singletons, pairwise independence of R_p,R_q makes both +coefficients zero. For one singleton and one triple, the triple's response +lies in W and the singleton's column lies outside W, so its coefficient +is zero. These exhaust every output equation that contains a singleton. +Every source coordinate on a singleton port appears at its own output +z=g rho_p. Consequently all source coordinates outside D vanish. + +This argument allows arbitrary partial intersections of the translated +outgoing sets. It assumes neither normality of H nor that those sets form +one common quotient partition after translation. + +## 3. Exact kernel on two blocks and their subblocks + +Once all singleton coordinates vanish, the source equation gives + +```text +x(g,p) = alpha(g) u_p, p in D. +``` + +There is no cross-block triple output. Therefore the later equations +reduce separately on B_1 and B_2 to + +```text +alpha(g) = alpha(g rho_a rho_b) = alpha(g rho_a rho_c). +``` + +Both products generate H. The right Cayley graph on each left coset is +connected, so alpha is constant separately on each block. Conversely each +constant triple vector has zero S and T, as in the cited one-block witness. +Their source supports are disjoint, so the vectors are independent. Thus + +```text +ker(S on B_1 union B_2) intersect ker(T on B_1 union B_2) + = span{1_(B_1) tensor u, 1_(B_2) tensor u}, +dimension = 2. +``` + +This holds for **every** pair of distinct left cosets. It is not a finite +enumeration of relative translations. + +For any A contained in B_1 union B_2, extend its inputs by zero. The theorem +then says that its kernel has dimension j, where j is the number of these +two cosets contained in A in full. Omitting any owner of one block forces +that block's constant amplitude to vanish. This is an immediate support +corollary, without an additional search or a hypothesis about missing outputs. + +For the cited 112-port, rank-eight reader, dim ker(S_A)=104|A|. Hence + +```text +rank(T_A restricted to ker(S_A)) = 104|A| - j. +``` + +This is the exact minimum number of additional **scalar linear** +observations that, together with S, determine the whole T field. A lower +count leaves an ambiguity in ker S outside ker T, even if postprocessing +is nonlinear. A linear quotient by the common kernel attains the count +abstractly. There is no assertion of efficient physical access or decoding. + +For two full source cosets, |A|=8160 and j=2, so the minimum is +848638. These are derived counts from the theorem and cited source order, +not a claim to have eliminated the full 913920-variable matrix. +The invisible fraction remains exactly 1/424320 of ker S. Pairing two +blocks cannot improve the single-block information-compression density. + +## 4. Executable corroboration and limits + +The source check establishes only condition 4 and the distinguished relation. +The other actual-source premises are inherited as stated in section 1. + +The new implication is corroborated over Q on G=S3 times C2, with +H=A3 times {0}. The three D routes are the three transpositions with zero +C2 bit. Two singleton routes are (identity,1) and (first transposition,1). +Their columns are e3 and e4, while the D columns are e1+e2,e1,e2. + +Exact elimination checks every pair of the four left cosets and every +subblock of one pair. Literal inherited vectors span the computed kernels. +The fixtures contain both possible overlapping class types, singleton with +singleton and singleton with triple. Controls separately place a singleton +inside W, make it parallel to a triple column, duplicate two singleton +columns, and discard later outputs outside the source. Each alteration +admits more than two directions on at least one enumerated two-coset block. +The receipt records the measured dimensions rather than assuming them. + +Three or more source cosets can contribute several singleton columns at +one output, permitting dependencies not excluded by this proof. This paper +does not decide that case, other triples' subgroups, or arbitrary owner +sets outside two left cosets. The rank-one-per-observation tariff, physical +acquisition, native phases, dirty restoration, storage, precision, compiler +and outer obligations remain separate. No new kappa or complete +multiplication theorem is claimed. diff --git a/research/centre-two-coset-separation/README.md b/research/centre-two-coset-separation/README.md new file mode 100644 index 0000000000..c51bf385a6 --- /dev/null +++ b/research/centre-two-coset-separation/README.md @@ -0,0 +1,107 @@ +# Two translated centre blocks have exactly two hidden directions + +For every pair of distinct left cosets of PR3828's 4080-owner subgroup, +the full scalar common-observation kernel is exactly the two known constant +triple directions, one per block. Pairing blocks creates no additional +hidden direction or improvement in information-compression density. + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: **scoped algebraic proof with finite corroboration**. This settles +the two-coset case of Open next question 1 in Clear1nsight's +[PR3828](https://github.com/CrocSwap/integer-mult-bounds/pull/3828). +The exact extra-linear-observation minimum on both full blocks is +`104*8160-2 = 848638`. For any subblock A of their union, the minimum is +`104|A|-j`, where j counts the complete cosets retained in A. + +[PROOF.md](PROOF.md) proves the result for every relative translation, +without assuming the subgroup is normal. At a later output, each block +contributes a singleton port or the distinguished triple. Two triple +contributions cannot meet. Distinct singleton columns cannot cancel each +other; a singleton also cannot cancel a vector in the triple plane. All +other ports vanish, leaving the inherited connected triple equations on +each block separately. + +The new source check proves that exactly ports `{0,6,85}` lie in that plane. +The single-block coset classification and order, reader rank and pairwise +column independence are cited predecessor premises. Their certificates are +not reverified. The theorem concerns the historical calls-0/4 scalar model, +not an automatically applicable replacement for the selected P104 word. + +## Reproduce + +From the repository root, CPython 3.12 and its standard library suffice. + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/centre-two-coset-separation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/centre-two-coset-separation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/centre-two-coset-separation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/centre-two-coset-separation --check-source-history +``` + +Any CPython 3.12 executable can replace the local interpreter path. +Expected markers are `PASS_CENTRE_TWO_COSET_SEPARATION`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +The direct check writes only stdout. Optional `--receipt /absolute/new/path` +writes a fresh receipt outside the package, binding every package file by +SHA256. No receipt is handwritten or committed. + +Exact source-column elimination checks 109 outside-plane columns. A new +small S3 times C2 model checks all six two-coset pairs and all 64 subblocks +of one pair, using literal matrices and kernel witnesses. Four controls +show why column separation and retaining all later outputs are necessary. +The proof supplies the universal result; these finite checks corroborate it. + +## Scope and credit + +The historical source order gives 8160 owners and a derived observation +minimum of 848638. The large source matrix is not replayed. Source-bound +metadata orientation passed on canonical main +`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. The selected +conditional kappa is `0.003125804` and is unchanged. + +Credit Chris R / Clear1nsight PR3828 for the question and full one-block +classification, Ross Richardson PR3797 for the parallel one-block proof +and observation interface, Matarener PR3656 for the subgroup and witness, +Sagar Thakrar PR3291 for the nonparallel-column premises, and Ross +Richardson PR3071 for the reader/model extraction convention. Retain David +Charbonneau PR3147, Sudarsh Chaturvedi PR3168, ywz65, Aaron Wang and the +selected native/geometry/compiler lineage credited by these packages. +No predecessor credit or frozen file is changed. + +No physical collector, recursive tariff, native implementation, improved +kappa or complete multiplication theorem is supplied. All five selected +framework assumptions remain. No Lean, Docker, selected cold replay or +independent human/formal-kernel review is claimed. + +## Open next questions + +Can three distinct left cosets have extra mixed kernel directions? At one +output, three singleton columns can be dependent, so the two-coset proof +ends there. First derive the actual outgoing incidences of one explicit +three-coset block and its coefficient compatibility. A useful physical +extension still needs source access, dirty restoration and a complete +paid/productive invoice; a scalar dimension is not a saved recursive call. + +## Implementation constraints + +Build the Lever supplies the source-plane checker and exact small-model +elimination. Prove It Works requires literal matrix kernels and controls +that break the stated hypotheses. No predecessor verifier is imported. + +Power of Ten review: no recursion, dynamic execution or subprocesses; +source prefix loops have exactly 10851 events times eight rows, and source +rank tests have eight rows and at most three columns. Small-model systems +have at most 72 rows and 30 columns. All functions are under 60 lines. +The source archive is hash-authenticated and bounded before decompression; +it contains no executable dependency. Receipts refuse existing destinations. +Explicit checks remain active under optimized Python. + +Rule 3 deviation: Python integers, Fraction and JSON/tar libraries allocate +dynamically. This is a bounded reference verifier, not a fixed-allocation +runtime. Bounds are eight MB for the authenticated archive, eight MB for +the decoded word, 704 live covector entries per row and 80-by-30 maximum +elimination storage. Runtime/library internal allocation is not instrumented. +The exact archive hash fixes decompression input before library allocation. +Warning-strict normal/optimized execution and AST parsing provide diagnostics; +no additional type checker or linter was run. diff --git a/research/centre-two-coset-separation/SOURCES.json b/research/centre-two-coset-separation/SOURCES.json new file mode 100644 index 0000000000..6e2238c2f8 --- /dev/null +++ b/research/centre-two-coset-separation/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/centre-sheaf-fibre/PROOF.md", + "usage": "provenance", + "git_blob": "f676ac48edfa05bfe959b4c83f556ab143f736bf", + "sha256": "f943dde4863c496020835da7e8d82515635f150a82c3eb4a0666e1ab8509c867" + }, + { + "path": "research/centre-sheaf-fibre/README.md", + "usage": "provenance", + "git_blob": "2c8168eee3c81c2a5c4598aa5629f98158b7d3ba", + "sha256": "31a7eedd13fd8abbbef475dba322cec3e30a0ee09b84d5c312c263d9a923057a" + }, + { + "path": "research/centre-coset-full-kernel/PROOF.md", + "usage": "provenance", + "git_blob": "f0e5ed2ed570a138ac3d734f51003e97486e4bb6", + "sha256": "c929ab00c3c018ced4d2ca776758bd1251f62630fa29f2f6a93c944a5d00c9ca" + }, + { + "path": "research/centre-block-moore-bound/PROOF.md", + "usage": "provenance", + "git_blob": "57e4adae5ab6247d7f82fefc2d91abccdb4bd39a", + "sha256": "4ff55b8d7c32f4ad2e32e267fd3e3340003b580dfa709577016eb605f157e137" + }, + { + "path": "research/centre-block-coset-kernel/README.md", + "usage": "provenance", + "git_blob": "f27dc04894b04dfbe60152adb77ac69b5b5f0628", + "sha256": "c7594aa840999aa366d834500f0b13cd870c215b321eacdfb0da43bc35d7eef6" + } + ] +} diff --git a/research/centre-two-coset-separation/TASK.json b/research/centre-two-coset-separation/TASK.json new file mode 100644 index 0000000000..38375a22a2 --- /dev/null +++ b/research/centre-two-coset-separation/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "centre-path-sharing", + "question": "Can a specified persistent boundary eliminate a repeated centre operation in the current caller?", + "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": "Write a two-call input/output contract on the current source word, including arbitrary centre baselines and every later read. Price producer, retention, native alignment and restoration jointly. Historical 64-per-call and 1.90x figures are not current budgets. Stop if a missing consumer or restored-input obligation consumes the saving; reopen only with a changed legal boundary.", + "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": [ + "centre path", + "persistent boundary", + "dirty recoding" + ], + "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": "Prove that any two distinct left cosets of the PR3828 centre subgroup have only their two inherited kernel directions; check the additional reader-plane premise and new small-group implication.", + "scope_change_reason": "Take PR3828 Open next question 1 as a historical scalar interface side result. This replaces the suggested verifier-engineering track with original mathematics and does not instantiate the current P104 two-call construction or reverify a predecessor.", + "bottleneck_link": "Centre sharing needs substantial independent information savings. This theorem rules out an improvement in compression density from pairing two of the known blocks; it makes no recursive tariff inference.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified two-coset result. Do not extend to three cosets or a physical collector.", + "outcome": "completed", + "evidence": "PROOF.md supplies the all-relative-translation theorem. verify.py checks 109 new source column-plane conditions, all six small-group two-coset systems, 64 subblocks and four hypothesis-sensitive controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can three distinct left cosets create additional mixed common-kernel directions?", + "why_it_matters": "Three singleton contributions can be dependent, so the two-coset separation theorem does not apply.", + "first_step": "Specify one exact three-coset incidence and compute the coefficient compatibility, with a stated source/consumer boundary.", + "blocked_by": "Actual mixed incidences and a favorable complete physical collector invoice are unknown." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241718", + "source_pr": 3828, + "source_author": "Clear1nsight", + "source_head": "4c379418cffa0ec5899c3af47c02d0f38813f7da" + }, + "family_gate": { + "decision": "narrow", + "reason": "A scoped algebraic side result, with no further construction or physical search. Acquisition/restoration/native/precision costs remain unknown." + }, + "upstream_checkpoint": { + "commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "checked_at": "2026-10-28T12:58:10Z" + }, + "environment": { + "python": "CPython 3.12.15", + "system": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "preserved_start": { + "branch": null, + "detached_head": "721c03822c421b7f7fcbb2598993b947c4d88419", + "prior_branch": "research/w1-1022ai-schur-intermediate-ranks", + "prior_branch_head": "acc000f4edfa0b0c4a90b505c6e02a4c3572f74c" + } +} diff --git a/research/centre-two-coset-separation/VERIFY.json b/research/centre-two-coset-separation/VERIFY.json new file mode 100644 index 0000000000..9d4e24562c --- /dev/null +++ b/research/centre-two-coset-separation/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New source reader-plane premise, six exact two-coset matrices, 64 subblocks, literal witnesses and four hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete scientific coverage and explicit controls under optimized Python." + } + ] +} diff --git a/research/centre-two-coset-separation/linear.py b/research/centre-two-coset-separation/linear.py new file mode 100644 index 0000000000..a854f306e0 --- /dev/null +++ b/research/centre-two-coset-separation/linear.py @@ -0,0 +1,36 @@ +"""Small exact linear algebra for the new two-coset fixtures. + +Produced by Nick Petalas. SPDX-License-Identifier: Apache-2.0 +""" +from fractions import Fraction + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + """Exact row rank; callers supply at most 80 rows and 30 columns.""" + need(len(rows) <= 80, "row limit") + width = len(rows[0]) if rows else 0 + need(width <= 30 and all(len(r) == width for r in rows), "matrix shape") + work = [[Fraction(x) for x in row] for row in rows] + pivot = 0 + for column in range(width): + found = next((i for i in range(pivot, len(work)) if work[i][column]), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + divisor = work[pivot][column] + work[pivot] = [x / divisor for x in work[pivot]] + for i in range(pivot + 1, len(work)): + coefficient = work[i][column] + work[i] = [x - coefficient * y for x, y in zip(work[i], work[pivot])] + pivot += 1 + return pivot + + +def apply(rows, vector): + need(all(len(row) == len(vector) for row in rows), "operator shape") + return [sum(x * y for x, y in zip(row, vector)) for row in rows] diff --git a/research/centre-two-coset-separation/reader.py b/research/centre-two-coset-separation/reader.py new file mode 100644 index 0000000000..dd3607171a --- /dev/null +++ b/research/centre-two-coset-separation/reader.py @@ -0,0 +1,81 @@ +"""Extract only the reader needed by the additional column-plane test. + +The archived prefix and query convention are credited to PR3071/3828. +No predecessor verifier, group census or single-block kernel replay runs. +Produced by Nick Petalas. SPDX-License-Identifier: Apache-2.0 +""" +from fractions import Fraction +from hashlib import sha256 +import gzip +import io +import json +import tarfile + +from linear import need, rank + +ARCHIVE = "research/community-frontier1094-audit/selected-replay.tar.gz" +ARCHIVE_HASH = "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" +MEMBER = "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz" +MEMBER_HASH = "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" + + +def source_word(root): + path = root / ARCHIVE + need(path.is_file() and not path.is_symlink(), "regular archive") + need(path.stat().st_size <= 8_000_000, "archive size limit") + raw = path.read_bytes() + need(sha256(raw).hexdigest() == ARCHIVE_HASH, "archive source hash") + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as archive: + members = archive.getmembers() + need(len(members) <= 10_000, "archive member limit") + matches = [member for member in members if member.name == MEMBER] + need(len(matches) == 1 and matches[0].isfile(), "unique regular word") + need(matches[0].size <= 2_000_000, "compressed word limit") + stream = archive.extractfile(matches[0]) + need(stream is not None, "word stream") + with stream: + packed = stream.read() + need(sha256(packed).hexdigest() == MEMBER_HASH, "word source hash") + decoded = gzip.decompress(packed) + need(len(decoded) <= 8_000_000, "decoded word limit") + return json.loads(decoded) + + +def reader_rows(word): + prefix = word["precondition"] + word["compensation"] + word["A"] + need(len(prefix) == 10851 and len(word["centers"]) == 8, "prefix contract") + result = [] + for center in word["centers"]: + need(type(center) is int and 0 <= center < 704, "center range") + row = [Fraction(0)] * 704 + row[center] = Fraction(1) + for event in reversed(prefix): + need(event[0] in ("add", "scale"), "prefix instruction") + target = event[1] + need(type(target) is int and 0 <= target < 704, "target range") + if event[0] == "scale": + need(len(event) == 5 and event[3] != 0, "scale shape") + row[target] *= Fraction(event[2], event[3]) + else: + need(len(event) == 6 and event[4] != 0, "addition shape") + source = event[2] + need(type(source) is int and 0 <= source < 704, "source range") + row[source] += Fraction(event[3], event[4]) * row[target] + result.append(row[:112]) + return result + + +def plane_certificate(root): + rows = reader_rows(source_word(root)) + a, b, c = 0, 6, 85 + need(all(r[a] == r[b] + r[c] for r in rows), "distinguished relation") + need(rank([[r[a], r[b]] for r in rows]) == 2, "triple plane rank") + outside = [] + for port in range(112): + value = rank([[r[a], r[b], r[port]] for r in rows]) + need(value == (2 if port in (a, b, c) else 3), "column-plane separation") + if port not in (a, b, c): + outside.append(port) + encoded = json.dumps([[str(x) for x in r] for r in rows], separators=(",", ":")) + return {"plane_ports": [a, b, c], "outside_plane_columns": len(outside), + "reader_sha256": sha256(encoded.encode()).hexdigest()} diff --git a/research/centre-two-coset-separation/verify.py b/research/centre-two-coset-separation/verify.py new file mode 100644 index 0000000000..aad38e9fef --- /dev/null +++ b/research/centre-two-coset-separation/verify.py @@ -0,0 +1,147 @@ +"""Corroborate two-coset separation, without replaying the cited block theorem. + +Produced by Nick Petalas. SPDX-License-Identifier: Apache-2.0 +""" +import argparse +from hashlib import sha256 +from itertools import combinations, permutations +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from linear import apply, need, rank # noqa: E402 +from reader import plane_certificate # noqa: E402 + + +def multiply(left, right): + p, bit = left + q, other = right + return tuple(p[q[i]] for i in range(3)), bit ^ other + + +def fixture(): + identity = (0, 1, 2) + group = [(p, b) for p in permutations(range(3)) for b in range(2)] + even = [p for p in permutations(range(3)) + if sum(p[i] > p[j] for i in range(3) for j in range(i + 1, 3)) % 2 == 0] + subgroup = {(p, 0) for p in even} + odd = [p for p in permutations(range(3)) if p not in even] + routes = [(p, 0) for p in odd] + [(identity, 1), (odd[0], 1)] + cosets = sorted({tuple(sorted(multiply(t, h) for h in subgroup)) for t in group}) + rows = [[1, 1, 0, 0, 0], [1, 0, 1, 0, 0], + [0, 0, 0, 1, 0], [0, 0, 0, 0, 1]] + need(len(group) == 12 and len(cosets) == 4, "fixture group") + need(all(multiply(r, r) == (identity, 0) for r in routes), "route involutions") + images = [{multiply(h, r) for h in subgroup} for r in routes] + need(images[0] == images[1] == images[2], "distinguished route class") + need(len({tuple(sorted(s)) for s in images}) == 3, "two singleton classes") + generator = multiply(routes[0], routes[1]) + need({(identity, 0), generator, multiply(generator, generator)} == subgroup, + "triple products generate subgroup") + for p, q in combinations(range(5), 2): + need(rank([[row[p], row[q]] for row in rows]) == 2, "nonparallel columns") + for p in (3, 4): + need(rank([[row[0], row[1], row[p]] for row in rows]) == 3, + "singleton outside triple plane") + return group, routes, cosets, rows + + +def joint_matrix(group, routes, rows, owners, retained_outputs=None): + variables = [(g, p) for g in sorted(owners) for p in range(5)] + old = [[rows[k][p] if g == owner else 0 for g, p in variables] + for owner in sorted(owners) for k in range(4)] + outputs = group if retained_outputs is None else retained_outputs + later = [[rows[k][p] if multiply(g, routes[p]) == output else 0 + for g, p in variables] for output in outputs for k in range(4)] + return variables, old, later + + +def check_block(group, routes, cosets, rows, owners): + variables, old, later = joint_matrix(group, routes, rows, owners) + complete = [set(c) for c in cosets if set(c) <= owners] + expected = len(complete) + actual = len(variables) - rank(old + later) + need(actual == expected, "complete-coset kernel dimension") + witnesses = [[(1, -1, -1, 0, 0)[p] if g in c else 0 for g, p in variables] + for c in complete] + need(rank(witnesses) == expected, "independent inherited directions") + for witness in witnesses: + need(not any(apply(old + later, witness)), "literal kernel witness") + return actual + + +def finite_checks(): + group, routes, cosets, rows = fixture() + full = [] + collision_types = set() + for first, second in combinations(cosets, 2): + owners = set(first) | set(second) + full.append(check_block(group, routes, cosets, rows, owners)) + for output in group: + counts = [sum(multiply(output, r) in c for r in routes) + for c in (set(first), set(second))] + if all(counts): + collision_types.add(tuple(sorted(counts))) + need(full == [2] * 6, "all two-coset fixtures") + need(collision_types == {(1, 1), (1, 3)}, "both mixed output-class cases") + universe = sorted(set(cosets[0]) | set(cosets[1])) + subset_dimensions = [] + for mask in range(1 << len(universe)): + owners = {g for i, g in enumerate(universe) if mask >> i & 1} + subset_dimensions.append(check_block(group, routes, cosets, rows, owners)) + return {"full_two_coset_systems": len(full), "subblocks": len(subset_dimensions), + "subblock_dimension_histogram": {str(k): subset_dimensions.count(k) + for k in sorted(set(subset_dimensions))}, + "collision_class_sizes": [list(t) for t in sorted(collision_types)]} + + +def controls(): + group, routes, cosets, rows = fixture() + owners = set(cosets[0]) | set(cosets[1]) + checks = [] + for column in ([1, 2, 0, 0], [1, 0, 0, 0], [0, 0, 0, 1]): + changed = [list(row) for row in rows] + for i in range(4): + changed[i][3] = column[i] + examples = [] + for left, right in combinations(cosets, 2): + block = set(left) | set(right) + variables, old, later = joint_matrix(group, routes, changed, block) + examples.append(len(variables) - rank(old + later)) + checks.append(max(examples)) + need(checks[0] > 2, "outside-plane premise is necessary") + need(checks[1] > 2, "nonparallel premise is necessary") + need(checks[2] > 2, "distinct singleton columns are necessary") + variables, old, later = joint_matrix(group, routes, rows, owners, owners) + dropped = len(variables) - rank(old + later) + need(dropped > 2, "whole-output premise is necessary") + return {"invalid_column_max_kernel_dimensions": checks, + "source_only_output_kernel_dimension": dropped} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = {"status": "PASS_CENTRE_TWO_COSET_SEPARATION", + "claim_type": "scoped proof with finite corroboration", + "new_reader_plane_check": plane_certificate(HERE.parents[1]), + "new_implication_fixtures": finite_checks(), "controls": controls(), + "derived_full_source_consequence": {"owners": 8160, "kernel_dimension": 2, + "minimum_extra_linear_observations": 848638}} + files = sorted(path for path in HERE.iterdir() if path.is_file()) + need(len(files) <= 16, "package file limit") + result["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt: + need(args.receipt.is_absolute() and HERE not in args.receipt.parents, + "receipt must be outside package") + with args.receipt.open("x") as stream: + need(stream.write(encoded) == len(encoded), "complete receipt write") + print(encoded, end="") + + +if __name__ == "__main__": + main()