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/char2-jets/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.
83 changes: 83 additions & 0 deletions research/char2-jets/MANIFEST.sha256
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE
2eeab89221c6ebc3e228d55aa279992b028ce19bfa7732ff808a601f81dd146a NOTICE.md
c1f20a1e7afb7eded3ff0ab765975f62466c5464ccaec143656319cdd4091945 README.md
55d864202535c22952e1a9080ad834f1908d18ff857c8dc26211e25a847d1fc8 c/enumall.c
a4e75f24543b3ae10f7ea4b03182e67e6b7998111ef8313dc95f20135652d264 checks/a_tprime.py
38fe007a75c5b942e1fc93fcc1ec2413c5f2213d1ea25a9180dcb0ae5ddeb56e checks/b_cr2.py
e4364436856f5b42fc8b2b662bdc03e161dd2f01938c0f0124f92155f90ef9b9 checks/c_jets.py
bd5530b6c6fca7fc794292e1b2beb9d13331df676dc8492f7e18a3fb5846c3d2 checks/common.py
2191412eb19afacb9f71dac4cc77fb8a25c86f7330238cbc0742c42ea39ac136 checks/d_lemmaA_B2.py
a8b13901e3b124888fd2bc397b6060d78559c4d7d11a37fe5c9927dcdb6b6ee6 checks/e_jetfail.py
4b3193ee81d7ac39d6c2e4b2d7597c5f485b17ca8b60d30c10b3d58bcadad468 checks/provenance.py
4c48f91787e8ee0407c218e3253ab38327cad0536128f73533edf864c9040891 data/aff14.json
89907be2205b217f5dfa79f6e12b19f05e52f158be301752a0ccfd3759151122 data/cech_v8.json
6ef2af941ccad9f8a1c38f3a26020425022b5b09e15183b52dc0a3651261cde8 data/cex_joint_v7.json
86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7 data/cex_min_1.json
9e92b7b5f1221c180af3637ff70940aca5255b92f7b641efe3c615433e54761a data/cex_wholeTS_v9.json
2ce114152529d375215f1f64a45072c9b78d1719d156e76bc692eff1fa955666 data/cr2_realisations.json
ea72716f98af4a99141d28f828db3c5c99c2cc8ad7d15ed6a8329de37ee36790 data/gad.json
cd8a8c2436e0a025348af0b52ccb48a4f64535b0ff8df32cbe13da73673266b7 data/jf0.json
b615b5c0916bf839e859fae3599c7ecb85881371a0cf1d55c1565e8e45afcd5a data/jf1.json
4baab4d953b56b20a138fb32650eca99fff1279f0cfaa0e4d674bc3fa3d219df data/jf2.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
f6d31a1f6e84a23ec615acd8828ea85acbdee885a832791b0514be6c424db5bb data/tied_min_B.json
b5aa8ca01a87a898ae27160d5274af7ff08127cf0b27cf372f73a5725cd216a5 data/tm_noncr2.json
f4e3f08ecd59aa64877bafc655d7cd58aea57418ce5d264107c6a5d4900585c7 evidence/PROOF-working-notes.md
560b3830c3f6d4764a156cde9f1447bfcacbfd3e4ce778a3b8c274a0a1482b5d lean/DecoderDuality.lean
ad4b7e6f8c06fbcc7d01d4e85828a4aa5de7280afd53c436ca7c8c938354b8df lean/README.md
9b4c0a346edd9d1362903bd0a32262fe0fb8e4f1f0ea3cbc2a66d700a7d4b3cb lean/lake-manifest.json
4b85c0ff74598a2970ff4a0a974971813a473361960bd5bedf09c14525186c4d lean/lakefile.toml
62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef lean/lean-toolchain
b9f4881da1cbad7c394a0a70614d62e4596b52bfde9967f8cd9aaa1279eaddde lib/col.py
ff3c1bbd072c4d1f47158f903aa3ff4fcd8db5bbc4709c3d15b21a1815eef3bd lib/cr2.py
4936fe52a5b996f91142c7fa0d8a1ca74f7c0e76ba9c3346748291c92e0940fa lib/gen.py
92fea2aca7b5298b30fb5ee176539a3887c0953728173c0fc1e26d55887b0f11 lib/gr.py
b7dc11f282395f40fb028249960e230598774680d0d73bfafd2166fe913f70ba lib/jet2.py
c707f5270b2eaef2da1dc0c1bf95c3ebf55d3fb667161c6c03a2126fad0422ec lib/kit.py
234e3a5f030bcc7356f582a85b8e02c6a02c18749d26ac222cc042b6ce198a08 lib/phi.py
cfbddbee3112f115c2ef606f7603481b4ef18cf80341041513a203417cc789e9 lib/satlib.py
afaae711d85b5508ee38efa8f23fa16774ec2c5c00f75c4687a9236841724772 lib/tangent.py
54424173c83403b81c7520f90197ba69dd32b17c02c54b3e0c927768e938453f requirements.txt
92281cc7387ca652203670976198add4131bb4df14a7e8f3c73fe87ec9e4153f scripts/make_data.py
b91c043adabcaf22c9cbe1729549c73406d49f87bb9062423f2678d57976cda3 scripts/t1.py
2bc5e670f02dba2cf177adef620fc63eade431c7b552bd3fd9ea0bbb24553987 scripts/t10.py
5106b0c310b3152e061df4c031b3774bf1e0aaac2831c8030ebc34f50755e607 scripts/t11.py
3e647cda0774ce7befb50110f1b02083859f730cf68f75f3064deab83f74c453 scripts/t12.py
f796de97a406d5069844f820f09d2fdb56afc43978fbf6d7957bd786d9cf29cb scripts/t13.py
5ba35faa15f53bdaa9bf99f35c67bcb131272d9627b8e4036fd6e01bfde56216 scripts/t14.py
f729950e9121c836c51e706dc04e44dfedb33f5464595c9604ca3f6c50d40bc7 scripts/t15.py
a23084d0b8d6a36356ddc3b57b1edab25b1d91e10d5f4380429c48ffc817aa47 scripts/t16.py
9aba9c011f3011fce22d5f5b6931c4613d5bf8a1340ffc091655f34e8ed5cd96 scripts/t17.py
aed231e657c62d4f347ffbf3ba93ae22a0ea3567f35ad3cc611cda90ccf8bf0b scripts/t18.py
83ac8a6dad9058f35ff12e61c9932688480be5b1cc2852004a5a28562d90cceb scripts/t19.py
c6c279f38df554c3cc7871019260935b99fe782a94f369d5ba808d5d78396698 scripts/t2.py
8c7bdfc55562ce2851102b872f127c01af06a45fdecd465bc2cf8b127b364b37 scripts/t20.py
8f7ef0cd3c0a6e74f2e11d1c82998b6947bcc03e7b2967433a126cfd7a1c3da5 scripts/t21.py
a590027e626d40f46e9eeb72077cda6872a998768bba8c07d17dbc3d709240df scripts/t22.py
60a7bee1d34be85fd6dc79b960f606be3541bd4cb39d36b6ab92ef7cfddb3afd scripts/t23.py
2e484e45e19dfd91fbeead52313b2dfffa011c796e96f5237d966c4309962453 scripts/t24.py
c9233cc4a134bd23dccaab3a982901a4fe503482e41537a68e196b4daaef3b2e scripts/t3.py
ba9ee091236742423eb698d0ef997c2190f7f4f8dd6cc03a05f533a9b3309e8f scripts/t4.py
fba0e1fc5364d94da884fd3c6b6c650bf8f337f0a8b60fb25cde1f1fabfa275d scripts/t5.py
a4904277d51abd4c9c5063cd282bb1f27915c96e7abaf73ee14420d6561c8f29 scripts/t6.py
69521b91da0ca0f07e1489895bb01bcb79fb9ba88bfaa8f40569f23486364050 scripts/t7.py
b3a4b48d5843e5b992b4ade587c4f1bae6f6bd4b5408d6134ac7e145c16c0a2e scripts/t8.py
785138735f8c27df1f4ea3af1083d321f063bb09ee0a975e0641713f58e51ad4 scripts/t9.py
cf9a793e3d6bdb5d033aa1b9c055feb87d093c60b4a08ebea9e8ec6558d067b6 scripts/tied_min_jet_cert.py
dbfb48fffcf2420aea8dad5e7c8b012fbfe2b19a3862d5dff8059cf31929e70b scripts/verify_cr2.py
31c4c9ca13073ae0723b90610cc0112554795456e49dde5611269332984d86d2 verify.sh
Loading
Loading