Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
201 changes: 201 additions & 0 deletions research/three-total-decoders/LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,201 @@
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/

TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION

1. Definitions.

"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.

"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.

"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.

"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.

"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.

"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.

"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).

"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.

"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."

"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.

2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.

3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.

4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:

(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and

(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and

(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and

(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.

You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.

5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.

6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.

7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.

8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.

9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.

END OF TERMS AND CONDITIONS

APPENDIX: How to apply the Apache License to your work.

To apply the Apache License to your work, attach the following
boilerplate notice, with the fields enclosed by brackets "[]"
replaced with your own identifying information. (Don't include
the brackets!) The text should be enclosed in the appropriate
comment syntax for the file format. We also recommend that a
file or class name and description of purpose be included on the
same "printed page" as the copyright notice for easier
identification within third-party archives.

Copyright [yyyy] [name of copyright owner]

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
61 changes: 61 additions & 0 deletions research/three-total-decoders/MANIFEST.sha256
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE
ccab919d95d1f5c137de9044897938188edddd967936ebcfff697ee32ab1c451 NOTICE.md
a812bb80e480a3f2f446e0f0f77300606e4337e4a888c141a7f4380ca15bef07 README.md
ad8545cd8408c80fc24ec82d3ebbe13b337ca66d0deabe388672b4e4b88c5558 SOURCES.json
9d5490a6bc5c9696e902075da2560d43abeef3d69c24b6dd05590d5d0fc93d35 c/brutetu.c
55d864202535c22952e1a9080ad834f1908d18ff857c8dc26211e25a847d1fc8 c/enumall.c
11f8c3d1ddb103eac91ef7c92e2dd887d53b5aa407997afba3105b01ac18bdc1 c/jsign.c
c1a69e5ca874d6a382583132f0596ddefb84f0e1b31b34775ca1c2aab32b95da c/mas.c
60e2538145cf3d0031ae29769b4c1a9a93fbcd252bed9163942cc5f1fd75bf2b c/tusign.c
fb18332a3adb4842c3662346aa7f6b5115debc04f1a392b6e9cbb423b7b83c8d checks/expect.py
c9b843903c6a1fb51e7a0664b010de0aa0a6cd66384b3ef39a71afb168b85285 checks/f2s.py
2c2d273387d6cd315e8606c8b5ffaa0421980d017c25f18df59177b3ef6277e1 checks/g1_cex.py
7b535510a03aa255e4ba78fd5787e58abbba214632966b6bba100cf1932cb10d checks/hesse_below.py
a656c6a54bc5cd1b3878dc63a020e25d910208e9fc6d347ffd0f6e968531a5b5 checks/hesse_smoke.py
0dc28b867ffa7d977aeb92cf9c71012030b4c27e0291b2a3659e8497622c3480 checks/lifts.py
0dc3997bdc78454b1e67e3d3c3798e4924817d311bbbc526d3554876d08a053c checks/mcc_cex.py
63cf4cb580ec56102a74680d226bc6f7993e233b3406ae409b6b19bcbc78f173 checks/nondeg.py
6b5d409e22d936c429f44595467939ef9e0dacedc73bc4ea177d7de2ba1770d3 checks/thm.py
e6d03be2481e30439f8bd2ab03c066b56025f89924f7309dab9dd59902da1f92 checks/tied_min.py
4c48f91787e8ee0407c218e3253ab38327cad0536128f73533edf864c9040891 data/aff14.json
89907be2205b217f5dfa79f6e12b19f05e52f158be301752a0ccfd3759151122 data/cech_v8.json
6ef2af941ccad9f8a1c38f3a26020425022b5b09e15183b52dc0a3651261cde8 data/cex_joint_v7.json
86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7 data/cex_min_1.json
15f5039069a175831f92c4ffe023a23a6f6e6bd6665f0ca2c2734bbe672b51ef data/cex_min_1.json.B22.json
9e92b7b5f1221c180af3637ff70940aca5255b92f7b641efe3c615433e54761a data/cex_wholeTS_v9.json
ea72716f98af4a99141d28f828db3c5c99c2cc8ad7d15ed6a8329de37ee36790 data/gad.json
312ee28adea5fba1b1d518271dfa57ef047a7b9c0560a57d397105ff49af2e12 data/gad_nonTS_minimiser.json
0eb5a156f3ca4c2fdbc43ad1004ade0897453702f25662837f33a0bf811d12da data/lifts_nojoint.json
201337647ca3012543ae326285fbf7a77d3e0b4290d156b72dde4e22e4186a3f data/mcc_cex_min_1_solution.json
7e5e5fa66dbaf0ac1fa7382fec28bbebe10d477e80022d648fb4c0093f23c64c data/nojoint_21_1.json
c56efcac1b354fca4efe5ce203c0df2c723e28b5acaf6600c53d65510f2aad5e data/nojoint_21_10.json
8315bda5e6e175c322c1db4767635c30c58a8095ff939b8555984da737fcd258 data/nojoint_21_11.json
a4ac2c9bfb72c2256032c5cde87860e0a82e78b4b788d0dae39d96e56dec7a58 data/nojoint_21_12.json
2d4ab6b67d6b17d8c231d6ddfaf58f1c73e34e1c8d622b69b133ac83b0a62b0b data/nojoint_21_13.json
b6ef1c334c38c805bfb8c33459db73f805da80a3e3bc64944a5542d75dafc4dd data/nojoint_21_14.json
6020caec4ce319e9ee122948b3e09ac987cba8f504ece906e550f3996e3d46a5 data/nojoint_21_2.json
d9531dccba8cad1ed6bce75e21ee1336d512969e73a53faff98718b3889b1ec3 data/nojoint_21_3.json
ba139ce8e3e65f429346a60015042ff2bffd25b91c7487a68d06f12457aba6b5 data/nojoint_21_4.json
e7cd06311ce71bd6460b3c6cf237eb9c19721ddc4c8cedd39ea736c1dfe1692f data/nojoint_21_5.json
9c7c2d30b33de6a34821ad853f455bbe9a8ca3c42707010c247dbef00575bca8 data/nojoint_21_6.json
d477bd3bafb872c2ba638183e34762d402f2c3687953360b137cc7222afa3f98 data/nojoint_21_7.json
99fd2dcbc1b52b1a7255cabe92e88508bccf936900d87f42108609bbc58952e4 data/nojoint_21_8.json
4b44af0cf900012124e1844f223abf1423c46d2561dce60a380d3957495d0e8e data/nojoint_21_9.json
2781dda2b8bc4d3ee75a2465cb7350973b514a9c737f9181e3bcff3f358ce839 data/supmin_fail_v8.json
670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93 data/tied_min.json
ef10f51b533d349ae465b1df2f46d367182264c22609d2d5cbfe3b7a6cfd7ff1 evidence/T3-PROOF.md
f91bbb764bb6c10a4348b3063000b3f773aeffc7dbe65c60e93a926794e5b4e8 evidence/cex-README.txt
5b11bc485ef50627e04fb790c463fba4ec31e851d788233ed0a4216938239a13 evidence/fleet-BRIEF.md
462fe8e9fa662365648e4f6fda3e029915a6e6b275b84f409670f35996098485 evidence/fleet-REQUESTS.md
791c7d53cb1b94cfe2674be0ffd5ba509fb1cf162ced5515ac0858fa23be1f91 evidence/fleet-S1.md
139f441a18e855e2761d2ec2ce0b53bcc2fad42d074368b02601f3bba8dc9882 evidence/fleet-S2.md
ba1ab38b52c84e59623ac33be6e5a7a8d5cf940d66047555905c366306861bb9 evidence/fleet-S3.md
cc1d9287fcdadb9afb670103fb18fac0d55664b6afd1673557aa60c217e59136 evidence/fprime-PROOF.md
304ff3ef8ef20093236d366b728acf570575050d1b9c64631bf3e5f7da668df8 evidence/g1-PROOF.md
7eb9e6735ff036533cfbdd86e5aa981d62a81a76deb95aeb2b61ddf3c6362c99 lib/hesse.py
c707f5270b2eaef2da1dc0c1bf95c3ebf55d3fb667161c6c03a2126fad0422ec lib/kit.py
cfbddbee3112f115c2ef606f7603481b4ef18cf80341041513a203417cc789e9 lib/satlib.py
427121d36b70d068fca3807e37868002f6271a9aa4eb465c18b347535040ba65 requirements.txt
b07eeaeeb537fecc75390ab832a5df4a629f9a1115bbd8cd40a77fd816a71d4c scripts/make_lifts.py
6c4c71c693e63a9b27b327c181d308878dd7c8ec966d70fea708e8bed4d9355b scripts/provenance.py
834a66a3fbd088400b1b4d063386ec8a2a62e0dd3d674aef1e952f4d9a25cf9e verify.sh
19 changes: 19 additions & 0 deletions research/three-total-decoders/NOTICE.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
# Notice

Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root).

## Credits (prior work this package stands on)

- **#446** (Theorem C; closed, not merged): the cost formula and exactness model; **#595** (FL C.6): the pairing model and the window table; **#717**: the provenance/manifest pattern of `scripts/provenance.py` and the complex E8 decoders; **#1590** (`research/root-unit-decoder-lemmas`, merged): Lemma A (T ≤ 2), the lift identity Lemma B, ERR1, the D5 CNF; `checks/expect.py` and `scripts/provenance.py` are adapted from that package. **#2031** (pending): the DRAT certificate of the D5 CNF, cited, not duplicated.
- Swarm work used, all from our own working cards of 2026-10-13/14: the second-prover card `KPR4-T3/PROOF.md` (L1–L8, Theorem P), the `fprime` card (Theorems M1, U, MCC, tied_min, SCC/Peel), fleet workers S1 (matroid route, TU-signability, gadget, aff14), S2 (F2S exchange route, PP, 4095 sub-configurations), S3 (adversary search), and the `g1` card (joint signability, counterexamples, Hesse runs). Their notes are shipped verbatim in `evidence/`.

## New in this package

`README.md`, `verify.sh`, `SOURCES.json`, `requirements.txt`, `MANIFEST.sha256`, `c/brutetu.c`, `lib/kit.py`, `lib/satlib.py`, `scripts/make_lifts.py` (adapted from the g1 card's `exactlift.py`), `data/lifts_nojoint.json`, `checks/*.py` (written for this package; they re-implement the checks of the working cards in exact arithmetic with fixed seeds), and the selection of data.

## Adapted from our earlier work

- `c/enumall.c`, `c/tusign.c`, `c/mas.c`: unchanged from the g1 and fprime cards. `c/jsign.c`: the g1 card's program with an added option that prints the solving signing.
- `lib/hesse.py`: the arithmetic and sampler of `g1/hesse.py` with the module-level search loop removed. `lib/satlib.py`: from `fprime/enumB.py` and `fprime/costsat2.py`.
- `data/`: configurations and certificates copied from the cards; `data/gad_nonTS_minimiser.json` is one entry of the card's list of 23552 gadget minimisers.
- `evidence/`: verbatim snapshots (snapshot of 2026-10-14 14:32; the status header of `g1-PROOF.md` predates its §11–14).
Loading
Loading