From 403158808f075dfafcd80da09f630b9a3fde6baa Mon Sep 17 00:00:00 2001 From: Hanson Sun <182361798+bbMisk@users.noreply.github.com> Date: Tue, 13 Oct 2026 22:05:44 -0400 Subject: [PATCH] Prove three-mode P112 COPY floor with exceptional erasures --- .../p112-three-mode-seed40/CERTIFICATE.json | 3424 +++++++++++++++++ research/p112-three-mode-seed40/CLAIM.json | 42 + .../p112-three-mode-seed40/INDEPENDENT.json | 194 + research/p112-three-mode-seed40/OVERLAP.json | 301 ++ research/p112-three-mode-seed40/README.md | 317 ++ research/p112-three-mode-seed40/SOURCES.json | 47 + research/p112-three-mode-seed40/TASK.json | 74 + .../p112-three-mode-seed40/VALIDATION.json | 182 + research/p112-three-mode-seed40/VERIFY.json | 40 + .../independent_check.py | 238 ++ .../p112-three-mode-seed40/test_package.py | 71 + research/p112-three-mode-seed40/verify.py | 361 ++ 12 files changed, 5291 insertions(+) create mode 100644 research/p112-three-mode-seed40/CERTIFICATE.json create mode 100644 research/p112-three-mode-seed40/CLAIM.json create mode 100644 research/p112-three-mode-seed40/INDEPENDENT.json create mode 100644 research/p112-three-mode-seed40/OVERLAP.json create mode 100644 research/p112-three-mode-seed40/README.md create mode 100644 research/p112-three-mode-seed40/SOURCES.json create mode 100644 research/p112-three-mode-seed40/TASK.json create mode 100644 research/p112-three-mode-seed40/VALIDATION.json create mode 100644 research/p112-three-mode-seed40/VERIFY.json create mode 100644 research/p112-three-mode-seed40/independent_check.py create mode 100644 research/p112-three-mode-seed40/test_package.py create mode 100644 research/p112-three-mode-seed40/verify.py diff --git a/research/p112-three-mode-seed40/CERTIFICATE.json b/research/p112-three-mode-seed40/CERTIFICATE.json new file mode 100644 index 0000000000..440e04b172 --- /dev/null +++ b/research/p112-three-mode-seed40/CERTIFICATE.json @@ -0,0 +1,3424 @@ +{ + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "claim": { + "active_terms_at_least": 3, + "all_coordinate_triples": 56, + "power_bill": "at least 8*8^q for 0= 2, |V| >= 2, B[U,V]=0. +``` + +For any `M in GL(4,C)`, set `N=M^(-T)` and + +```text +D=[Y,u] M, T=[Y,v] N. +``` + +Ordinary transpose gives `DT^T=YY^T+uv^T`. Thus the four terms, together with +the other five coordinate terms, obey the masked decoder identity on every +constrained entry `B_ij=1`. All choices of complex amplitudes on U,V are +included. A support container with zeros is allowed only if the actual +supports still satisfy the displayed size conditions. + +**Theorem.** If `r_j=rho(supp(D[:,j]),supp(T[:,j]))`, at least three r_j are +at least eight. Consequently + +```text +40 + sum_(j=0)^3 r_j >= 64, +5*8^q + sum_(j=0)^3 r_j^q >= 8*8^q (0 < q <= 1). +``` + +Identity mixing attains equality with ranks `(8,8,8,0)` for every admissible +u,v. If all four projected products defined below are active, the whole COPY +sum is at least 72. No claim of sharpness for that all-active subcase is made. + +## All complex support patterns, without coefficient sampling + +Seed 40 selects lexicographic coordinate triple number 40: `(2,4,5)`. +The 112 projected rows on these coordinates have 13 nonzero projective +directions: all `{0,+1,-1}^3` directions, modulo sign. For a nonzero complex +coefficient vector a, the directions annihilating a span a proper rational +flat of rank zero, one, or two. They are exactly the available directions in +that flat. Rational ranks remain unchanged over C. + +There are one rank-zero, 13 rank-one, and 25 rank-two flats: **39 supports**. +For rank two, the primary checker enumerates cross products of every pair of +independent directions. For rank one it constructs a vector annihilating that +direction and no other; it also constructs a generic vector annihilating +none. These representatives certify support patterns, not a bounded search +over possible complex coefficients. The second checker independently closes +proper row spaces by rational RREF, starting from the zero space. It obtains +the same 39 supports without using cross products or importing their producer. + +Three supports, the coordinate supports, have binary row-span dimension eight; +the other 36 have dimension nine. The 39-by-39 unmodified pairing table has +every entry at least eight. The table is stored and recomputed exactly. + +## The four exceptions to two-anchor span preservation + +Write `N(b)={i:B_ib=0}` and let S be one of the 39 supports. Every linear +functional on the row space of B has evaluations on its rows in +`col(B)=row(B)`. Thus the complete 512-element row space supplies all binary +separating characters c. Examine the nonempty cuts +`E=S intersect supp(c)`. Counting character-support pairs, the census is: + +| Common odd neighbors of E | Nonempty cuts | +|---:|---:| +| 0 | 15,210 | +| 1 | 4,712 | +| 2 | 4 | + +Every exceptional cut has size 24 and equals `N(b) intersect N(c)` for its +two common odd neighbors. The original support has row-span dimension nine; +erasing that cut leaves dimension eight. In the specified sorted root order: + +| Coefficients on (2,4,5) | Two anchors | Span before / after | +|---|---|---| +| (1,-1,-1) | (8,16) | 9 / 8 | +| (1,-1,1) | (9,17) | 9 / 8 | +| (1,1,-1) | (14,22) | 9 / 8 | +| (1,1,1) | (15,23) | 9 / 8 | + +The certificate gives all four erased sets and their separating character. +Each exceptional survivor set pairs at rank **exactly eight with every one +of the 39 unmodified supports**. + +Suppose `B[U,V]=0`, with both supports of size at least two, and erasing U +from S lowers its full binary row span. A separating character has a nonempty +cut E contained in U. Every member of V is a common odd neighbor of E. +The census therefore forces E to be an exceptional cut and V to be exactly +its two anchors. Then `U` is contained in their common odd neighborhood, +which equals E. Since E is already contained in U, **U=E and |V|=2**. +This classifies every possible span loss, including arbitrary smaller +erasures and complex amplitudes. + +The independent checker reaches the same classification by a different finite +reduction. It tests the maximal deletion `N(b) intersect N(c)` for every +unordered anchor pair and every support: + +| Span before / after | Support and anchor-pair cases | +|---|---:| +| 8 / 8 | 18,648 | +| 9 / 9 | 223,772 | +| 9 / 8 | 4 | + +These 242,424 cases exhaust 39 times 6,216. For each exception, restoring +**any one** of its 24 erased rows restores dimension nine. Hence every proper +subset of that deletion preserves span. The four erased sets have exactly +their indicated two common odd neighbors. These checks independently justify +the arbitrary-U classification above, without relying on the character census. + +## Paired support bound and the four-term cost argument + +For any two strata S,T and admissible U,V, + +```text +rho(S minus U, T minus V) >= 8. (1) +``` + +If both deletions preserve full row/column spans, restricting spanning rows +to the surviving columns, and then using the preserved column span, leaves +the original pairing rank unchanged. It is at least eight by the table. + +If the left span drops, the classification forces U to be one exceptional +24-row cut and V its two anchors. A two-element V cannot be an exceptional +24-row erasure, so the right column span is preserved. Restriction to the +exceptional left survivor set therefore gives its certified pairing rank +eight. The symmetric case is identical. Both spans cannot drop at once, +because one drop forces the opposite erasure to have size two. This proves +(1) despite the failure of unconditional span preservation. + +Write the j-th columns of M,N as `(a_j,c_j)` and `(b_j,d_j)`, with +`a_j,b_j in C^3`. The top-left block of `MN^T=I_4` gives + +```text +sum_j a_j b_j^T = I_3. +``` + +At least three summands are nonzero rank-one products, because the right side +has rank three. Call these products active. For each active j, `Ya_j` and +`Yb_j` have supports S,T from the complete classification. Corrections can +cancel entries only on U,V, so the actual term supports contain +`S minus U` and `T minus V`. Matrix rank is monotone under enlarging index +sets. Equation (1) therefore gives `r_j>=8`. Remaining terms stay in the bill +with nonnegative cost. This proves the theorem and both cost inequalities. + +The certificate supplies 56 explicit permutations of the eight frame +coordinates carrying `(2,4,5)` to every unordered triple. Both checkers verify +each signed root-line bijection and every binary pairing entry, as well as +complete triple coverage. Row signs do not change supports; the corresponding +sign changes to arbitrary u,v are allowed. Reordering the three modes is +absorbed into M. Thus the representative proof applies to all 56 triples +without assuming a group-classification theorem. + +## Controls, optimistic budget, and limits + +The literal exceptional cancellation has ranks `(8,8,8,6)` and whole COPY +sum 70. Omitting its compensation changes constrained entry `(4,9)`. This +illustrates why a span drop alone is not a saving. Other fixtures cover +nonreal rational coefficients, transposition, permutation, identity mixing, +and a 2-by-2 correction. The mathematical controls reject a wrong inverse +transpose, Hermitian substitution, singular mixing, a nonfree correction, +and an invalid coordinate transport. A one-anchor example lowers a coordinate +span from eight to seven; it marks a proof boundary and does not refute any +separate singleton COPY theorem. + +Six external tests reject an omitted support stratum, omitted exception, +forged COPY63 claim, invalid transport, missing geometry pin, and changed +geometry bytes. They invoke the checkers with `-I -O -B`; explicit failures +remain active with assertions disabled. + +The blocked objective is lowering the separate COPY charge while retaining +the other charges and normalization. For fixed width m and common remaining +bill C, the affected optimistic contribution satisfies + +```text +C + sum_j (r_j/m)^q >= C + 3*(8/m)^q. +``` + +All four replacement terms are counted. Granting zero additional preparation, +source access, frame changes, helper work, restoration, hosting, and recursive +management still cannot improve this objective. No physical implementation or +complete supplier recurrence is asserted. Savings in other work, a different +normalization or a legal sharing convention could change the question. + +The finite evidence supports the written quantified argument; it is not a +formal proof of the full multiplication theorem. All-size compilation, +common-label/mutable-source realization, physical frames/owners, whole-call +hosting, precision/tape, exact recovery, analytic transfer, and the retained +bit H1-H5 obligations are outside this result. + +## Provenance, overlap, and credit + +Exact base: `ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. +The selected record, its source manifest, actual construction and maintainer +review identify conditional `kappa=836330098538459/500000000000000000`, +with the complex primitive binding. The baseline source-binding check was run; +the selected cold replay is not needed for this additive research package and +is not claimed. Selected, frozen, and upstream inputs remain unchanged. + +[CLAIM.json](CLAIM.json) records OS-random seed 40, three candidate tasks, +the local claim, exact scope, budget and stop rule. No pinned coordination +issue existed. The initial complete overlap snapshot covered 745 open PRs +and 174 discussions. [OVERLAP.json](OVERLAP.json) records the final refresh; +search coverage is not proof of novelty. + +Direct predecessor: Hanson Sun / [PR1473](https://github.com/CrocSwap/integer-mult-bounds/pull/1473), +head `ea2f6bf0940580dfaeb393ec0786abc8f7bbb7b4`, poses the three-mode question +and proves the two-mode span lemma. The new proof cannot assume that lemma for +three modes: the four counterexamples above are real. PR1432 supplies earlier +boundary/coupled-factor work. PR1460 and Gareth Davidson / bitplane's PR1468 +address two-mode arbitrary and singleton-sided corrections, respectively; +neither theorem is imported here. + +Credit commdata2338 / PR1375, Cinna Davis / PR1373 and Arham Tahir / PR1331 +for the preceding rectangle and compensation questions; Mihir Srivastava / +PR845 for the pinned geometry implementation used only by the primary +checker; DreamingOfClouds / PR717 and PR446/595 for the decoder and COPY +framework; themilkman216 / PR968 for the pairing-cost model; Joel Pulikkan / +GamingPuzzled / PR620 for the coordinate COPY64 construction; and woklerx / +PR1077 for the complex-coefficient orientation check. The nearby PR1325 +sparse-lift result keeps fixed readers and concerns a different class. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex** +assistance in mathematics, both implementations, verification and writing. +New work is Apache-2.0; predecessor attribution and licenses are retained. + +## Open next questions + +- **Singleton-sided corrections with three modes.** A 24-row cut can coexist + with more freedom on a singleton side, so the two-anchor classification does + not settle this case. First classify one-anchor losses among these 39 + strata, then test the coupled four-term bill. The missing step is a bound + on compensation, not a larger search inside the proved class. +- **Four coordinate modes with one correction.** This changes the projected + coefficient rank and support arrangement. First enumerate its proper + rational flats and identify which free erasures change pairings before + trying `GL(5,C)` synthesis. The 39-stratum lemma and four-term rank argument + do not transfer automatically; complete helper/physical costs remain open. + +[TASK.json](TASK.json) gives the relevance, first step and blocker for each. diff --git a/research/p112-three-mode-seed40/SOURCES.json b/research/p112-three-mode-seed40/SOURCES.json new file mode 100644 index 0000000000..9ddddb519e --- /dev/null +++ b/research/p112-three-mode-seed40/SOURCES.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-decoder-field-extension-seed44/PROOF.md", + "usage": "input", + "git_blob": "4a3063de8fe606a88bd5bdb9b7d2e5dccb70f73f", + "sha256": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2" + }, + { + "path": "research/p112-single-lift/PROOF.md", + "usage": "input", + "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1" + }, + { + "path": "research/p112-single-lift/geometry.py", + "usage": "input", + "git_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "sha256": "3857c11ec731a602b8059d85d58fbb3b641bab687bb33016a0e54f7567752c8a" + } + ], + "context_sources": [ + { + "pr": 1473, + "head": "ea2f6bf0940580dfaeb393ec0786abc8f7bbb7b4", + "path": "research/p112-multiline-free-rectangles-seed42/README.md", + "url": "https://github.com/bbMisk/integer-mult-bounds/blob/ea2f6bf0940580dfaeb393ec0786abc8f7bbb7b4/research/p112-multiline-free-rectangles-seed42/README.md", + "sha256": "dd01a5f293c9f5f3ede914feb00827063a3d6ff5b2036b5204c7581d1eb386e0", + "git_blob": "909971c944b14754f28a345d309c0fb3fb0385fa", + "usage": "Reviewed context and question attribution only. No pending theorem or source code is imported." + } + ] +} diff --git a/research/p112-three-mode-seed40/TASK.json b/research/p112-three-mode-seed40/TASK.json new file mode 100644 index 0000000000..373796d6df --- /dev/null +++ b/research/p112-three-mode-seed40/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "One arbitrary complex B-free rank-one correction with both actual supports of size at least two, mixed with any three P112 coordinate modes by GL(4,C); separate COPY rank and power bill.", + "scope_change_reason": "The user assigned structural decoder research by OS seed 40. PR1473 leaves three-mode supports open; this changes the number of simultaneously mixed original modes from two to three and handles four new span-loss exceptions. Explicit symmetries extend the seed-selected triple (2,4,5) to all 56 triples.", + "bottleneck_link": "The complex primitive binds. A smaller separate COPY bill could help a changed decoder; the optimistic relaxation already fails in this scoped three-mode class, so no supplier construction is pursued.", + "budget_minutes": 60, + "stop_rule": "One 60-minute session from 2026-10-14T01:35Z; orientation at most 12 minutes; reserve final 15 minutes for verification and handoff. Stop construction if a proved COPY floor excludes the optimistic bill. No stochastic synthesis or unbounded search.", + "outcome": "negative-result", + "evidence": "README quantified proof; CERTIFICATE.json exact 39-stratum character census and four exceptions; INDEPENDENT.json complete maximal-erasure census and 96 restoration identities; six exact fixtures, corruption controls, source pins and registered replay.", + "author": "Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation of both checkers, verification and writing. Both implementations have the same AI-assisted author; no independent human review or proof assistant.", + "open_questions": [ + { + "question": "Can a singleton-sided free correction mixed with three coordinate modes lower the separate COPY bill?", + "why_it_matters": "This removes the two-anchor premise and changes the geometric loss and compensation possibilities.", + "first_step": "Classify one-anchor erasures for the 39 exact support strata, then price the coupled four-term compensation.", + "blocked_by": "The present paired-span proof requires both supports to have at least two elements; no compensation lower bound for this broader class is supplied." + }, + { + "question": "What happens when four coordinate modes are mixed with one free correction?", + "why_it_matters": "A different projected rank/support arrangement may change copied-information cost on the binding complex side.", + "first_step": "Enumerate the proper rational flats on one coordinate quadruple and classify free erasures before attempting GL(5,C) synthesis.", + "blocked_by": "The 39-stratum classification does not apply, and any positive decoder would still need a complete physical invoice." + } + ], + "assignment_seed": 40, + "seed_method": "OS-backed secrets.randbelow(100)", + "representative_triple": [ + 2, + 4, + 5 + ], + "completed_domain": "All 39 complex support strata; 512 binary characters per stratum; 6216 anchor pairs per stratum independently; all 56 coordinate triples by explicitly verified symmetries. Written rank argument covers all admissible complex amplitudes and GL(4,C), not a finite coefficient search." +} diff --git a/research/p112-three-mode-seed40/VALIDATION.json b/research/p112-three-mode-seed40/VALIDATION.json new file mode 100644 index 0000000000..dc309373ca --- /dev/null +++ b/research/p112-three-mode-seed40/VALIDATION.json @@ -0,0 +1,182 @@ +{ + "status": "local scoped checks passed; see scope and unrun obligations", + "checked_at": "2026-10-14T02:03:35.141414+00:00", + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "selected_kappa": "836330098538459/500000000000000000", + "python_registered": "Python 3.12.13", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "runs": [ + { + "name": "registered", + "command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/p112-three-mode-seed40" + ], + "exit_code": 0, + "seconds": 11.69, + "log": "registered.log" + }, + { + "name": "workflow-tests", + "command": [ + "python3.12", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_research_*.py", + "-v" + ], + "exit_code": 0, + "seconds": 2.383, + "log": "workflow-tests.log" + }, + { + "name": "selected-record", + "command": [ + "make", + "selected-record-check" + ], + "exit_code": 0, + "seconds": 0.606, + "log": "selected-record.log" + }, + { + "name": "baseline", + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "exit_code": 0, + "seconds": 0.341, + "log": "baseline.log" + } + ], + "read_only_relocation": { + "python": "Python 3.14.6", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "file_count": 13, + "all_file_hashes_unchanged": true, + "files": { + "research/complex-decoder-field-extension-seed44/PROOF.md": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2", + "research/p112-single-lift/PROOF.md": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1", + "research/p112-single-lift/geometry.py": "3857c11ec731a602b8059d85d58fbb3b641bab687bb33016a0e54f7567752c8a", + "research/p112-three-mode-seed40/CERTIFICATE.json": "63d844896913e264747d0bca8233c1705e43b998dec10eaed1eadbc207c992c6", + "research/p112-three-mode-seed40/CLAIM.json": "8293b082745634bae1a9e7b9f0cb0a58818a6816050a3f63b4645fb7afd17d89", + "research/p112-three-mode-seed40/INDEPENDENT.json": "25b1dd3b1b8df613cffd31a2e39062ab4aa83b019db305c7bc9b13a33854a699", + "research/p112-three-mode-seed40/README.md": "ca6b23d64f53086b0095c0104c2ea559198bdab8f943ce4c2722bb45207c548a", + "research/p112-three-mode-seed40/SOURCES.json": "445ba664bd697ddeba5c25f0bd5cb619b576e552982e3ca91d9ccc1f0d6722ee", + "research/p112-three-mode-seed40/TASK.json": "2ca45f1a4990f83726a6971c298f6784f5509ddd8893d68d0e11c946c97e6f32", + "research/p112-three-mode-seed40/VERIFY.json": "ee056db8d31ead5afef5ba253bc5beab5767b22eb42c2417b88763bc8fcf02b5", + "research/p112-three-mode-seed40/independent_check.py": "a85226417278a1c53f8d1a9fa19980a3678e3a477a98ee958c24e2c4b8c0dcb4", + "research/p112-three-mode-seed40/test_package.py": "e44f759c84616afc5f5644ab36d9a06b2b9bdbfb0d778758b25f9d9852fdc446", + "research/p112-three-mode-seed40/verify.py": "c48553a004e07f65a5b41cc9394dc7e503378d2e49fc48b196e08d90d70009f5" + }, + "runs": [ + { + "script": "verify.py", + "command": [ + "python3", + "-I", + "-O", + "-B", + "/research/p112-three-mode-seed40/verify.py" + ], + "exit_code": 0, + "seconds": 1.281, + "stdout": "PASS_P112_THREE_MODE_COPY strata=39 cuts=19926 exceptions=4 triples=56 COPY=64 controls=8", + "stderr": "" + }, + { + "script": "independent_check.py", + "command": [ + "python3", + "-I", + "-O", + "-B", + "/research/p112-three-mode-seed40/independent_check.py" + ], + "exit_code": 0, + "seconds": 3.038, + "stdout": "PASS_INDEPENDENT_THREE_MODE strata=39 erasures=6216 span_checks=242424 exceptions=4 restored=96 COPY=64", + "stderr": "" + } + ] + }, + "upstream_compatibility": { + "base": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "latest_main": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "source_comparison": [ + { + "path": "certificates/selected-result.json", + "base_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "latest_main_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "unchanged": true + }, + { + "path": "docs/research/agent-task-catalog.json", + "base_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "latest_main_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "unchanged": true + }, + { + "path": "research/complex-decoder-field-extension-seed44/PROOF.md", + "base_blob": "4a3063de8fe606a88bd5bdb9b7d2e5dccb70f73f", + "latest_main_blob": "4a3063de8fe606a88bd5bdb9b7d2e5dccb70f73f", + "unchanged": true + }, + { + "path": "research/p112-single-lift/PROOF.md", + "base_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "latest_main_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "unchanged": true + }, + { + "path": "research/p112-single-lift/geometry.py", + "base_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "latest_main_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "unchanged": true + } + ] + }, + "checked_file_sha256": { + "README.md": "ca6b23d64f53086b0095c0104c2ea559198bdab8f943ce4c2722bb45207c548a", + "verify.py": "c48553a004e07f65a5b41cc9394dc7e503378d2e49fc48b196e08d90d70009f5", + "independent_check.py": "a85226417278a1c53f8d1a9fa19980a3678e3a477a98ee958c24e2c4b8c0dcb4", + "test_package.py": "e44f759c84616afc5f5644ab36d9a06b2b9bdbfb0d778758b25f9d9852fdc446", + "CERTIFICATE.json": "63d844896913e264747d0bca8233c1705e43b998dec10eaed1eadbc207c992c6", + "INDEPENDENT.json": "25b1dd3b1b8df613cffd31a2e39062ab4aa83b019db305c7bc9b13a33854a699", + "SOURCES.json": "445ba664bd697ddeba5c25f0bd5cb619b576e552982e3ca91d9ccc1f0d6722ee", + "TASK.json": "2ca45f1a4990f83726a6971c298f6784f5509ddd8893d68d0e11c946c97e6f32", + "VERIFY.json": "ee056db8d31ead5afef5ba253bc5beab5767b22eb42c2417b88763bc8fcf02b5" + }, + "counts": { + "primary_support_strata": 39, + "nonempty_character_support_cuts": 19926, + "span_loss_exceptions": 4, + "triple_transports": 56, + "gaussian_rational_fixture_entries": 75264, + "primary_controls": 8, + "independent_span_checks": 242424, + "independent_single_row_restorations": 96, + "independent_controls": 5, + "external_corruption_tests": 6, + "research_workflow_tests": 20 + }, + "unrun": [ + "Full selected-supplier cold replay", + "New native or hosted physical supplier admission", + "Proof-assistant formalization", + "Independent human mathematical review", + "Hosted CI success at local packaging time" + ], + "scope": "The checkers verify finite geometric premises and fixtures for the README written theorem. No new kappa, physical recurrence, universal decoder lower bound or full multiplication theorem is claimed. The local timing is not a performance claim.", + "attribution": "Hanson Sun (@bbMisk), substantial OpenAI Codex assistance; both implementations have the same AI-assisted author." +} diff --git a/research/p112-three-mode-seed40/VERIFY.json b/research/p112-three-mode-seed40/VERIFY.json new file mode 100644 index 0000000000..faa2b2071f --- /dev/null +++ b/research/p112-three-mode-seed40/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-decoder-field-extension-seed44/PROOF.md", + "research/p112-single-lift/PROOF.md", + "research/p112-single-lift/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact complex support strata, exhaustive character cuts, four exceptions, all-triple transports, six Q(i) fixtures and eight controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 180, + "checks": "Code-disjoint Euclidean geometry, rational flats, all 242424 maximal-erasure comparisons, 96 restoration identities and integer compensation." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Six externally exercised source/certificate corruption tests with optimized isolated subprocesses." + } + ] +} diff --git a/research/p112-three-mode-seed40/independent_check.py b/research/p112-three-mode-seed40/independent_check.py new file mode 100644 index 0000000000..d11c588e01 --- /dev/null +++ b/research/p112-three-mode-seed40/independent_check.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Code-disjoint finite-premise check: Euclidean roots, rational flats, erasures. + +No primary/predecessor code imports; proposed transport/certificate witnesses +are data and are checked. Same AI-assisted author, not independent human review. +Hanson Sun (@bbMisk), substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + +HERE=Path(__file__).resolve().parent +TRIPLE=(2,4,5) + + +def check(ok, message): + if not ok: raise ValueError(message) + + +def rank_sets(rows, ceiling=None): + pivots={} + for original in rows: + row=set(original) + while row: + first=min(row) + if first not in pivots: + pivots[first]=row + if ceiling is not None and len(pivots)==ceiling: return len(pivots) + break + row.symmetric_difference_update(pivots[first]) + return len(pivots) + + +def echelon(rows): + a=[list(map(Fraction,row)) for row in rows if any(row)] + cursor=0 + for j in range(3): + found=next((i for i in range(cursor,len(a)) if a[i][j]),None) + if found is None: continue + a[cursor],a[found]=a[found],a[cursor] + value=a[cursor][j];a[cursor]=[v/value for v in a[cursor]] + for i in range(len(a)): + if i!=cursor: + value=a[i][j];a[i]=[v-value*w for v,w in zip(a[i],a[cursor])] + cursor+=1 + return tuple(tuple(row) for row in a[:cursor]) + + +def build(): + roots=set() + for i,j in combinations(range(8),2): + for sign in (-1,1): + row=[0]*8;row[i]=2;row[j]=2*sign;roots.add(tuple(row)) + for signs in product((-1,1),repeat=7): + if sum(v==-1 for v in signs)%2==0: roots.add((1,)+signs) + frame=[] + for j in range(4): + for sign in (1,-1): + row=[0]*8;row[2*j]=2;row[2*j+1]=2*sign;frame.append(tuple(row)) + check(len(roots)==120 and set(frame)<=roots,'root/frame enumeration') + roots=sorted(roots-set(frame)) + x=[[sum(a*b for a,b in zip(row,f))//4 for f in frame] for row in roots] + gram=[[sum(a*b for a,b in zip(r,s))//4 for s in roots] for r in roots] + b=[{j for j,g in enumerate(row) if (g+1)%2} for row in gram] + check(len(roots)==112 and all(sum(v*v for v in row)==8 for row in roots),'root norms') + check(all(sum(a*c for a,c in zip(x[i],x[j]))==2*gram[i][j] + for i in range(112) for j in range(112)),'XX^T identity') + check(rank_sets(b)==9,'binary pairing rank') + # Echelon pivot columns give an injective projection of the full row space. + pivots={} + for original in b: + row=set(original) + while row: + j=min(row) + if j in pivots: row.symmetric_difference_update(pivots[j]) + else: pivots[j]=row;break + columns=set(pivots) + short=[row & columns for row in b] + check(len(columns)==9 and rank_sets(short)==9,'injective full-row projection') + return roots,x,b,short + + +def flats(x): + projected=[tuple(row[k] for k in TRIPLE) for row in x] + directions=sorted(set(echelon([row]) for row in projected if any(row))) + known={()};pending=[()] + while pending: + current=pending.pop() + for direction in directions: + new=echelon(current+direction) + if len(new)<=2 and new not in known: + known.add(new);pending.append(new) + inventory={} + for flat in known: + support=frozenset(i for i,row in enumerate(projected) + if len(echelon(flat+(row,)))>len(flat)) + check(support not in inventory,'duplicate proper-flat support') + inventory[support]=len(flat) + check(len(directions)==13 and len(inventory)==39,'proper-flat enumeration') + return inventory + + +def compute(certificate): + roots,x,b,short=build() + source=json.loads((HERE/'SOURCES.json').read_text()) + check(source['base_commit']==certificate['base_commit'],'base binding') + for row in source['files']: + if row['usage']=='input': + data=(HERE.parents[1]/row['path']).read_bytes() + check(hashlib.sha256(data).hexdigest()==row['sha256'],'source drift: '+row['path']) + rowbits=[sum(1< 0 else tuple(-x for x in vector) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def cross(a, b): + return (a[1]*b[2]-a[2]*b[1], a[2]*b[0]-a[0]*b[2], a[0]*b[1]-a[1]*b[0]) + + +def check_sources(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_text()) + rows = sources['files'] + paths = [row['path'] for row in rows] + require(len(paths) == len(set(paths)), 'duplicate source pins') + require({row['path'] for row in rows if row['usage'] == 'input'} == { + GEOMETRY, 'research/p112-single-lift/PROOF.md', + 'research/complex-decoder-field-extension-seed44/PROOF.md'}, + 'incomplete live source inventory') + for row in rows: + if row['usage'] != 'input': + continue + p = ROOT / row['path'] + require(p.resolve().is_relative_to(ROOT.resolve()), 'external source path') + data = p.read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source SHA256: ' + row['path']) + blob = b'blob ' + str(len(data)).encode() + b'\0' + data + require(hashlib.sha1(blob).hexdigest() == row['git_blob'], 'source Git blob: ' + row['path']) + return sources + + +def geometry(): + spec = importlib.util.spec_from_file_location('pinned_p112_geometry', ROOT / GEOMETRY) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + raw = module.build() + module.check_geometry(raw) + order = sorted(range(112), key=lambda i: max(tuple(raw['roots'][i]), tuple(-x for x in raw['roots'][i]))) + roots, x, labels, duals = [], [], [], [] + for i in order: + root = raw['roots'][i] + sign = 1 if tuple(root) > tuple(-z for z in root) else -1 + roots.append(tuple(sign*z for z in root)) + x.append(tuple(sign*z for z in raw['X'][i])) + labels.append(raw['labels'][i]) + duals.append(raw['duals'][i]) + b = [[(duals[i] & labels[j]).bit_count() % 2 for j in range(112)] for i in range(112)] + require(len(set(roots)) == 112 and len(set(labels)) == 112, 'duplicate root/label') + for i in range(112): + for j in range(112): + require(dot(roots[i], roots[j]) % 4 == 0, 'nonintegral Gram') + gram = dot(roots[i], roots[j]) // 4 + require(dot(x[i], x[j]) == 2*gram, 'XX^T != 2G') + require(b[i][j] == (1+gram) % 2, 'binary pairing binding') + return module, roots, x, labels, duals, b + + +def support_strata(x): + rows = [tuple(row[j] for j in TRIPLE) for row in x] + normals = sorted({canonical(r) for r in rows} - {None}) + coeffs = {canonical(cross(a,b)) for a,b in combinations(normals, 2)} - {None} + # Representatives of every rank-one zero flat and the generic zero flat. + for normal in normals: + found = next((a for a in product(range(-4,5), repeat=3) + if any(a) and dot(a,normal) == 0 + and all(dot(a,n) != 0 for n in normals if n != normal)), None) + require(found is not None, 'no rank-one flat representative') + coeffs.add(canonical(found)) + found = next((a for a in product(range(1,6), repeat=3) + if all(dot(a,n) != 0 for n in normals)), None) + require(found is not None, 'no generic representative') + coeffs.add(canonical(found)) + supports = {} + for a in sorted(coeffs): + mask = bm(i for i,r in enumerate(rows) if dot(r,a)) + supports.setdefault(mask, a) + require(len(normals) == 13 and len(supports) == 39, 'arrangement coverage') + return normals, [(a,s) for s,a in sorted(supports.items(), key=lambda item: item[1])] + + +def transports(x, b): + tetrads = {bm(j for j,v in enumerate(r) if v) for r in x} + root_lookup = {max(r,tuple(-v for v in r)): i for i,r in enumerate(x)} + require(len(root_lookup) == 112 and len(tetrads) == 14, 'frame-coordinate root coverage') + found = {} + for perm in permutations(range(8)): + destination = tuple(sorted(perm[k] for k in TRIPLE)) + if destination in found: + continue + if not all(bm(perm[j] for j in bits(t)) in tetrads for t in tetrads): + continue + mapping, signs = [], [] + for row in x: + new = [0]*8 + for j in range(8): + new[perm[j]] = row[j] + new = tuple(new) + key = max(new,tuple(-v for v in new)) + require(key in root_lookup, 'transport does not preserve root lines') + i = root_lookup[key] + mapping.append(i) + signs.append(1 if new == x[i] else -1) + require(len(set(mapping)) == 112, 'transport is not a bijection') + require(all(b[i][j] == b[mapping[i]][mapping[j]] for i in range(112) for j in range(112)), + 'transport changed binary pairing') + found[destination] = {'destination': list(destination), 'permutation': list(perm), + 'line_map_sha256': hashlib.sha256(json.dumps([mapping, signs]).encode()).hexdigest()} + if len(found) == 56: + break + require(set(found) == set(combinations(range(8),3)), 'incomplete triple transport') + return [found[k] for k in sorted(found)] + + +# Exact Gaussian-rational fixture arithmetic. Examples check conventions; +# the arrangement/rank proof, not sampling, gives the complex quantifier. +Z, O, I = (0,0), (1,0), (0,1) + + +def ga(a,b): return (a[0]+b[0], a[1]+b[1]) +def gn(a): return (-a[0],-a[1]) +def gm(a,b): return (a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]) +def gc(a): return (a[0],-a[1]) + + +def gd(a,b): + norm = b[0]*b[0]+b[1]*b[1] + require(norm != 0, 'singular Gaussian division') + z = gm(a,gc(b)) + out = (Fraction(z[0],norm), Fraction(z[1],norm)) + return tuple(v.numerator if v.denominator == 1 else v for v in out) + + +def identity(n): return [[O if i==j else Z for j in range(n)] for i in range(n)] +def transpose(m): return list(map(list,zip(*m))) + + +def mm(a,b): + out=[] + for row in a: + outrow=[] + for col in zip(*b): + value=Z + for v,w in zip(row,col): value=ga(value,gm(v,w)) + outrow.append(value) + out.append(outrow) + return out + + +def inverse(m): + n=len(m) + rows=[list(r)+e for r,e in zip(m,identity(n))] + for k in range(n): + pivot=next((i for i in range(k,n) if rows[i][k] != Z),None) + require(pivot is not None,'singular mixing') + rows[k],rows[pivot]=rows[pivot],rows[k] + v=rows[k][k] + rows[k]=[gd(z,v) for z in rows[k]] + for i in range(n): + if i!=k: + v=rows[i][k] + rows[i]=[ga(z,gn(gm(v,w))) for z,w in zip(rows[i],rows[k])] + return [r[n:] for r in rows] + + +def free_support(left,right,b): + require(left.bit_count()>=2 and right.bit_count()>=2,'fixture support premise') + require(all(not b[i][j] for i in bits(left) for j in bits(right)),'nonfree fixture') + + +def fixtures(x,b,pairrank,exceptions): + e=exceptions[0] + U=set(e['erasure']); V=set(e['anchors']) + a=e['coefficient'] + w=[sum(row[TRIPLE[j]]*a[j] for j in range(3)) for row in x] + u=[(w[i],0) if i in U else Z for i in range(112)] + v=[O if i in V else Z for i in range(112)] + cancel=identity(4) + for k in range(3): cancel[k][0]=(a[k],0) + cancel[3][0]=(-1,0) + complex_m=identity(4) + for i,j,c in [(0,1,I),(1,2,(Fraction(1,2),0)),(2,3,(1,-1)),(3,0,(2,1)),(0,2,(-1,1))]: + shear=identity(4);shear[i][j]=c;complex_m=mm(complex_m,shear) + swap=identity(4);swap[0],swap[2]=swap[2],swap[0] + cases=[('identity',u,v,identity(4)),('exceptional_cancellation',u,v,cancel), + ('nonreal_dense',u,v,complex_m),('permuted',u,v,swap), + ('transpose_nonreal',v,u,transpose(complex_m)), + ('small_rectangle',[O if i in sorted(U)[:2] else Z for i in range(112)],v,complex_m)] + receipts=[]; controls=[]; saved={} + for name,left,right,m in cases: + us=bm(i for i,z in enumerate(left) if z!=Z);vs=bm(i for i,z in enumerate(right) if z!=Z) + free_support(us,vs,b) + A=[[(row[k],0) for k in TRIPLE]+[left[i]] for i,row in enumerate(x)] + C=[[(row[k],0) for k in TRIPLE]+[right[i]] for i,row in enumerate(x)] + n=transpose(inverse(m));D=mm(A,m);T=mm(C,n) + target=mm(A,transpose(C));actual=mm(D,transpose(T)) + require(actual==target,'fixture factor identity') + ranks=[pairrank(bm(i for i in range(112) if D[i][j]!=Z), + bm(i for i in range(112) if T[i][j]!=Z)) for j in range(4)] + active=[any(m[k][j]!=Z for k in range(3)) and any(n[k][j]!=Z for k in range(3)) for j in range(4)] + require(sum(active)>=3 and all(not active[j] or ranks[j]>=8 for j in range(4)), + 'fixture contradicts active-term bound') + receipts.append({'name':name,'support_sizes':[us.bit_count(),vs.bit_count()], + 'replacement_ranks':ranks,'active_projected_products':sum(active), + 'whole_copy_sum':40+sum(ranks),'entries_checked':112*112}) + saved[name]=(A,C,m,D,T,target) + require(receipts[0]['replacement_ranks']==[8,8,8,0],'identity attainment') + A,C,m,D,T,target=saved['exceptional_cancellation'] + omitted=mm([r[:3] for r in D],transpose([r[:3] for r in T])) + fail=next(((i,j) for i in range(112) for j in range(112) if b[i][j] and omitted[i][j]!=target[i][j]),None) + require(fail is not None,'omitted compensation control did not fail') + controls.append({'name':'omit_compensation','constrained_entry':list(fail)}) + wrong=mm(D,transpose(mm(C,inverse(m)))) + fail=next(((i,j) for i in range(112) for j in range(112) if b[i][j] and wrong[i][j]!=target[i][j]),None) + require(fail is not None,'wrong inverse-transpose control did not fail') + controls.append({'name':'wrong_inverse_transpose','constrained_entry':list(fail)}) + A,C,m,D,T,target=saved['nonreal_dense'] + wrong=mm(D,[[gc(v) for v in r] for r in transpose(T)]) + fail=next(((i,j) for i in range(112) for j in range(112) if b[i][j] and wrong[i][j]!=target[i][j]),None) + require(fail is not None,'Hermitian control did not fail') + controls.append({'name':'Hermitian_in_place_of_transpose','constrained_entry':list(fail)}) + singular=identity(4);singular[3]=singular[0][:] + try: inverse(singular) + except ValueError: controls.append({'name':'singular_mixing'}) + else: raise ValueError('singular matrix accepted') + badcol=next(j for j in range(112) if any(b[i][j] for i in U)) + try: free_support(bm(U),bm(V | {badcol}),b) + except ValueError: controls.append({'name':'nonfree_correction','added_column':badcol}) + else: raise ValueError('nonfree correction accepted') + return receipts,controls + + +def compute(): + sources=check_sources() + g,roots,x,labels,duals,b=geometry() + normals,strata=support_strata(x) + row_bits=[bm(j for j,v in enumerate(row) if v) for row in b] + chars=sorted({bm(i for i in range(112) if (duals[i]&q).bit_count()%2) for q in range(512)}) + require(len(chars)==512 and len(g.binary_basis(row_bits))==9,'character coverage') + require(all(row in chars for row in row_bits),'character space binding') + odd=[ALL ^ row for row in row_bits] + def rank(mask): return len(g.binary_basis(labels[i] for i in bits(mask))) + def pairrank(left,right): + lb=g.binary_basis(duals[i] for i in bits(left)) + rb=g.binary_basis(labels[j] for j in bits(right)) + return len(g.binary_basis(sum(((v&w).bit_count()%2)<=8 for row in table for v in row),'original pairing floor') + controls=[{'name':'reject_three_mode_span_preservation','counterexamples':len(exceptions)}] + axis=bm(i for i,row in enumerate(x) if row[TRIPLE[0]]) + beta=next(j for j in range(112) if rank(axis & ~odd[j])