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
2 changes: 1 addition & 1 deletion .github/workflows/verify.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ jobs:
fail-fast: false
matrix:
python-version: ['3.11', '3.13', '3.14']
group: [community, producers, certificates, ternary, research, tests]
group: [community, skip, producers, certificates, ternary, research, tests]
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
with:
Expand Down
27 changes: 26 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,22 @@ community-audit-check:
community-followup-check:
python3 scripts/audit_followup_candidate.py --candidate-root . --check docs/research/community-followup-arithmetic.json

.PHONY: verify-community verify-producers verify-certificates verify-ternary verify-tests
.PHONY: verify-community verify-skip verify-producers verify-certificates verify-ternary verify-tests
# CI runs these in separate checkouts. Keep local verification sequential:
# different groups regenerate certificates that another group may read.
verify:
$(MAKE) verify-community
$(MAKE) verify-skip
$(MAKE) verify-producers
$(MAKE) verify-certificates
$(MAKE) verify-ternary
$(MAKE) verify-research
$(MAKE) verify-tests

verify-skip:
$(MAKE) skip-strips-verify
$(MAKE) skip-clones-verify

verify-community: community-audit-check community-followup-check copied-reversed-producer copied-reversed-check copied-fixed-reversed-producer copied-fixed-reversed-check
$(MAKE) copied-fixed-verify
$(MAKE) climbed-48-verify
Expand Down Expand Up @@ -269,6 +274,26 @@ copied-fixed-check:

copied-fixed-verify: copied-fixed-producer copied-fixed-check

.PHONY: skip-strips-verify skip-strips-producer skip-strips-check
skip-strips-producer:
python3 research/skip-strips/producer.py

skip-strips-check:
python3 research/skip-strips/audit.py
python3 research/skip-strips/verify.py --output research/skip-strips/certificate.json
cd research/skip-strips && python3 -m unittest discover -s ../../tests -p 'test_skip_strips.py' -v

skip-strips-verify: skip-strips-producer skip-strips-check

.PHONY: skip-clones-verify skip-clones-producer skip-clones-check
skip-clones-producer:
python3 research/skip-clones/producer.py

skip-clones-check:
python3 research/skip-clones/witness.py --output research/skip-clones/certificate.json
python3 -m unittest discover -s tests -p 'test_skip_clones.py' -v

skip-clones-verify: skip-clones-producer skip-clones-check
.PHONY: climbed-48-verify climbed-48-producer climbed-48-check
climbed-48-producer:
python3 research/climbed-48/producer.py
Expand Down
21 changes: 21 additions & 0 deletions NOTICE
Original file line number Diff line number Diff line change
Expand Up @@ -203,3 +203,24 @@ Ryan S / princezuda contributes historical Lean certificate arithmetic, algebrai
frame/movement/guard lemmas and independent paired-circuit checks (#26). Original
source notices and historical snapshots are preserved. Neither formal package
claims a full formal proof of the multiplication algorithm or a new kappa.

Skip-prefix strip producer, 8 October 2026
By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5)
assistance. The skip-prefix leave-one-out strip layout in
research/skip-strips/skip_graph.py is new. Everything else reuses Chafik
Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification
code, exact data recovery and support-order sorting, together with:
- Rohan Arun's PR #44 weighted carrier matching optimizer;
- RaD (hipotures) PR #41 alternating point order;
- every predecessor credited above.
Complete attribution and the conditional proof boundary are recorded in
research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain
applicable.

Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones):
Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain
source-partition clone operation is adapted from RaD / hipotures, PR #51,
with original envelopes retained here. The scalar base is Avi Eisenberg's
PR #53 skip-prefix layout, prepared with Anthropic Claude assistance.
All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain
in force. This extension is provided under the repository's Apache-2.0 terms.
27 changes: 27 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,33 @@ AI-assistance disclosures remain credited in the source notices.
[Maintainer review](docs/research/community-followup-review.md) ·
[Integration record](docs/research/community-followup-integration.md)

## Additional conditional circuit result: PR #54

The [paid-clone construction](research/skip-clones/PROOF.md) gives
**κ = 141532521/3125000000000 = 4.529040672e-5 > 2^-15**, conditional on
OpenAI's base theorem and the retained analytic and fixed-tape interfaces.
This branch result is additional to the maintainer-reviewed PR #49 witness
above; it does not extend that review's scope or claim global optimality.

Starting from Avi Eisenberg's [PR #53 skip-prefix strips](research/skip-strips/PROOF.md),
606 explicitly paid whole-chain clones preserve the original core/cover
envelopes. The pinned weighted matchings give R23=32693, R25=43056 and
W=159592676, with every added operation charged and both complete dirty-basis
orientations replayed. The conditional saving is 0.686876% above PR #53.
The source-partition/whole-chain operation is adapted from RaD / hipotures
(PR #51); this original-envelope specialization is by Chafik Boukhalfa with
OpenAI Codex assistance. All predecessor notices remain in force.

PR #53 itself reassociates each leave-one-out strip as
`s_j = A_(j-2) + (v_(j-1) + B_(j+1))`, preserving every scalar term while
creating nested consumer envelopes. Its matched roles are R23=32946 and
R25=43409, giving W=160799739 and conditional κ=4498144/10^11.

Run `make verify-skip` for both complete producer replays and their exact
arithmetic and adversarial checks, or `make skip-clones-verify` for PR #54.
Local `make verify` and every Python-version CI matrix include these checks
alongside all reviewed community and historical checks.

## What changed

The community work combines recursive batching and partial-swap frames with
Expand Down
15 changes: 9 additions & 6 deletions docs/ci-verification.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,18 @@ The Python 3.13 log shows these major sequential costs:
| Prime-field network certificate | 83 seconds |
| Endpoint-gauge producer regeneration | 54 seconds |

The workflow now distributes each Python version across six independent
The workflow now distributes each Python version across seven independent
checkouts:

| Make target | Coverage |
|---|---|
| `verify-community` | PR #39 and follow-up arithmetic, reversed/fixed producers, PR #48 and #49 complete replays |
| `verify-skip` | PR #53 skip-prefix and PR #54 paid-clone complete producers, exact arithmetic, and focused adversarial tests |
| `verify-producers` | Copied-center, structured-bulk, endpoint-gauge and partial-swap producers and certificates |
| `verify-certificates` | Remaining exact arithmetic, historical constructions and research audits |
| `verify-ternary` | Complex-compression and ternary checkpoint audits and patches |
| `verify-research` | 28 recovered historical audits and their regenerated certificates |
| `verify-tests` | All 419 current and recovered tests and all 20 historical patch-application checks |
| `verify-tests` | All current and recovered tests and all 20 historical patch-application checks |

Every group runs on **all three** Python versions (3.11, 3.13 and 3.14).
Both pinned Lean packages remain separate jobs. No producer replay, negative
Expand All @@ -32,13 +33,15 @@ regenerated artifact cannot silently diverge from its recorded certificate.

At the original five-group split, `make -n verify` expands to the same multiset of
**94 leaf commands**, including identical multiplicities for duplicate checks.
That split changed scheduling rather than mathematics or certificate inputs.
The subsequent research reconciliation adds 28 audit commands (122 total leaf
commands) and additional tests; it does not remove any existing check.
The original split changed scheduling rather than mathematics or certificate inputs.
The additional `verify-skip` group preserves those commands and adds the
PR #53/#54 producer, exact checker and focused adversarial tests. The research
reconciliation adds all 28 recovered audit commands and additional tests.
Both additions remain in the combined workflow; no existing check is removed.
The complete old run remains useful as a comparison; the new workflow must
pass independently in clean checkouts.

Local `make verify` invokes the six groups sequentially. Do not launch them
Local `make verify` invokes the seven groups sequentially. Do not launch them
concurrently in the same worktree: one group can read certificates another
group regenerates. CI avoids that race by using a separate runner and checkout
for each group. Directly invoking a group works from a fresh checkout; the
Expand Down
Loading