Skip to content

Integrate opt-in prefix capacity into the corrected census successor #5033

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 23, 2026
Merged

Integrate opt-in prefix capacity into the corrected census successor #5033

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
129 changes: 129 additions & 0 deletions research/f7-prefix-capacity-engine/DELTA.diff
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
--- vendor/union_census.c
+++ census.c
@@ -1,4 +1,8 @@
-/* Corrected finite canonical restored-word census with a union-support budget.
+/* Source-bound maintained-engine successor with opt-in prefix capacity.
+ * JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0.
+ * PR5001 capacity theorem: Ali Romman; all predecessor credit follows.
+ *
+ * Corrected finite canonical restored-word census with a union-support budget.
* Derived from Nicholas Stone's corrected_census.c (research/
* f7-weight-parity-census-correction, sha256 265ead91...) and the L<=22 gate
* extension recorded in PR #3731; preserves the restricted-growth word scope.
@@ -51,11 +55,12 @@
typedef unsigned __int128 mask_t;
typedef struct { char key[L+1]; int length; uint64_t cap; } Shard;
typedef struct {
- uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes, union_prunes;
+ uint64_t nodes, candidate_leaves, hits, even_prunes, odd_prunes, union_prunes, capacity_prunes;
int aborted;
double seconds;
} Result;
static int S,T, even_on=1,odd_on=1,union_on=1,even_budget,odd_budget,union_budget;
+static int capacity_on,capacity_active;
static int word[L], counts[N], E[L+1],O[L+1],es=1,os=0;
static int q,used,odd_counts,even_excess,odd_excess;
static mask_t seen=1, ee,oo,eo;
@@ -69,6 +74,46 @@
}
static inline int parity(int x) { return __builtin_popcount((unsigned)x)&1; }
static inline mask_t bit(int x) { return (mask_t)1 << x; }
+/* The caller supplies a simple path; each omitted functional uses actual splits. */
+static uint32_t capacity_splits(int depth,int omitted) {
+ int k=depth+1,r=L-k,mask=((1<<N)-1)^(1<<omitted);
+ int size[2]={0},stays[2]={0},cheap[2]={0},pairs[2]={0},available[2]={0};
+ int point=0,crossing=0;
+ size[0]=1;
+ for(int i=0;i<depth;i++) {
+ int next=point^(1<<word[i]);
+ int side=parity(next&mask);
+ size[side]++;
+ if(word[i]==omitted) stays[side]++; else crossing++;
+ point=next;
+ }
+ if(!r) return __builtin_popcount((unsigned)q)==1 ? (uint32_t)1<<size[0] : 0;
+ for(int vertex=0;vertex<(1<<N);vertex++) if(!(seen&bit(vertex))) {
+ int side=parity(vertex&mask),mate=vertex^(1<<omitted);
+ available[side]++;
+ if(mate==0 || mate==q) cheap[side]++;
+ else if(!(seen&bit(mate)) && vertex<mate) pairs[side]++;
+ }
+ uint32_t splits=0;
+ for(int x=0;x<=r;x++) {
+ int added[2]={x,r-x},low=crossing,high=crossing+r+1;
+ if(x>available[0] || r-x>available[1]) continue;
+ if(size[0]+x && size[1]+r-x && low<2) low=2;
+ for(int side=0;side<2;side++) {
+ int one=cheap[side]<added[side]?cheap[side]:added[side];
+ int two=(added[side]-one)/2;
+ if(two>pairs[side]) two=pairs[side];
+ int total=size[side]+added[side];
+ int floor=2*total-2*(stays[side]+one+two);
+ int ceiling=2*total-2*stays[side];
+ if(low<floor) low=floor;
+ if(high>ceiling) high=ceiling;
+ }
+ low+=low&1;
+ if(low<=high) splits|=(uint32_t)1<<(size[0]+x);
+ }
+ return splits;
+}
static void rec(int i) {
if (run.aborted || io_error) return;
if (current->cap && run.nodes >= current->cap) { run.aborted=1; return; }
@@ -84,6 +129,11 @@
return;
}
if (odd_counts+2*(N-used)>L-i) return;
+ if(capacity_active && i>0) {
+ for(int omitted=0;omitted<N;omitted++) if(!capacity_splits(i,omitted)) {
+ run.capacity_prunes++; return;
+ }
+ }
int limit=used<N ? used+1 : N;
for (int j=0;j<limit;j++) {
if (run.aborted || io_error) return;
@@ -166,14 +216,15 @@
static void write_result(FILE *f,const char *prefix,Result *r,int comma) {
fprintf(f," {\"prefix\":\"%s\",\"nodes\":%" PRIu64 ",\"candidate_restored_leaves\":%" PRIu64 ",\"all_restored_leaves\":",prefix,r->nodes,r->candidate_leaves);
if (!even_on&&!odd_on&&!r->aborted) fprintf(f,"%" PRIu64,r->candidate_leaves); else fputs("null",f);
- fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"union_budget_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->union_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":"");
+ fprintf(f,",\"hits\":%" PRIu64 ",\"even_budget_prunes\":%" PRIu64 ",\"odd_budget_prunes\":%" PRIu64 ",\"union_budget_prunes\":%" PRIu64 ",\"prefix_capacity_prunes\":%" PRIu64 ",\"aborted\":%s,\"complete\":%s,\"seconds\":%.6f}%s\n",r->hits,r->even_prunes,r->odd_prunes,r->union_prunes,r->capacity_prunes,r->aborted?"true":"false",(!r->aborted&&!io_error)?"true":"false",r->seconds,comma?",":"");
}
int main(int argc,char **argv) {
Shard shards[128]; Result results[128]; int nshards=0;
const char *hits_path=NULL,*json_path=NULL; uint64_t cap=0;
- if (argc<2||!parse_split(argv[1])) { fprintf(stderr,"usage: %s s,t --hits PATH [--json PATH] [--cap N] [--no-budgets|--no-even-budget|--no-odd-budget] [PREFIX[:CAP]...]\n",argv[0]); return 1; }
+ if (argc<2||!parse_split(argv[1])) { fprintf(stderr,"usage: %s s,t --hits PATH [--json PATH] [--cap N] [--prefix-capacity] [--no-budgets|--no-even-budget|--no-odd-budget] [PREFIX[:CAP]...]\n",argv[0]); return 1; }
for (int a=2;a<argc;a++) {
const char *arg=argv[a];
+ if (!strcmp(arg,"--prefix-capacity")) { capacity_on=1; continue; }
if (!strcmp(arg,"--no-budgets")) { even_on=odd_on=union_on=0; continue; }
if (!strcmp(arg,"--no-even-budget")) { even_on=0; continue; }
if (!strcmp(arg,"--no-odd-budget")) { odd_on=0; continue; }
@@ -197,6 +248,7 @@
if (!strncmp(shards[a].key,shards[b].key,(size_t)common)) { fprintf(stderr,"overlapping shards\n"); return 1; }
}
}
+ capacity_active=capacity_on && N>=2 && L>=4 && L<=(1<<N) && S==L/2 && T==L/2;
even_budget=S*(S-1)/2+T*(T-1)/2-((1<<(N-1))-1);
odd_budget=S*T-(1<<(N-1));
union_budget=S*(S-1)/2+T*(T-1)/2-((1<<(N-1))-1);
@@ -220,14 +272,15 @@
run.seconds=(double)(end.tv_sec-start.tv_sec)+1e-9*(double)(end.tv_nsec-start.tv_nsec);
results[a]=run; done++;
total.nodes+=run.nodes; total.candidate_leaves+=run.candidate_leaves; total.hits+=run.hits;
- total.even_prunes+=run.even_prunes; total.odd_prunes+=run.odd_prunes; total.union_prunes+=run.union_prunes;
+ total.even_prunes+=run.even_prunes; total.odd_prunes+=run.odd_prunes; total.union_prunes+=run.union_prunes; total.capacity_prunes+=run.capacity_prunes;
total.aborted|=run.aborted; total.seconds+=run.seconds;
printf("SHARD %s nodes=%" PRIu64 " candidate_restored_leaves=%" PRIu64 " hits=%" PRIu64 " complete=%s seconds=%.3f\n",current->length?current->key:"-",run.nodes,run.candidate_leaves,run.hits,(!run.aborted&&!io_error)?"true":"false",run.seconds); fflush(stdout);
if (run.aborted||io_error) break;
}
printf("TOTAL N=%d L=%d split=%d,%d nodes=%" PRIu64 " candidate_restored_leaves=%" PRIu64 " hits=%" PRIu64 " complete=%s seconds=%.3f\n",N,L,S,T,total.nodes,total.candidate_leaves,total.hits,(!total.aborted&&!io_error)?"true":"false",total.seconds);
if(jsonout) {
- fprintf(jsonout,"{\n \"schema\":1,\"n\":%d,\"length\":%d,\"split\":[%d,%d],\"groups\":\"hamming_weight_parity\",\"even_budget\":%d,\"odd_budget\":%d,\"union_budget\":%d,\"even_budget_enabled\":%s,\"odd_budget_enabled\":%s,\"union_budget_enabled\":%s,\n \"complete\":%s,\"aborted\":%s,\"requested_shards\":%d,\"completed_or_partial_shards\":%d,\n \"shards\":[\n",N,L,S,T,even_budget,odd_budget,union_budget,even_on?"true":"false",odd_on?"true":"false",union_on?"true":"false",(!total.aborted&&!io_error)?"true":"false",total.aborted?"true":"false",nshards,done);
+ fprintf(jsonout,"{\n \"prefix_capacity_requested\":%s,\"prefix_capacity_enabled\":%s,\n",capacity_on?"true":"false",capacity_active?"true":"false");
+ fprintf(jsonout," \"schema\":1,\"n\":%d,\"length\":%d,\"split\":[%d,%d],\"groups\":\"hamming_weight_parity\",\"even_budget\":%d,\"odd_budget\":%d,\"union_budget\":%d,\"even_budget_enabled\":%s,\"odd_budget_enabled\":%s,\"union_budget_enabled\":%s,\n \"complete\":%s,\"aborted\":%s,\"requested_shards\":%d,\"completed_or_partial_shards\":%d,\n \"shards\":[\n",N,L,S,T,even_budget,odd_budget,union_budget,even_on?"true":"false",odd_on?"true":"false",union_on?"true":"false",(!total.aborted&&!io_error)?"true":"false",total.aborted?"true":"false",nshards,done);
for(int a=0;a<done;a++) write_result(jsonout,shards[a].key,&results[a],a+1<done);
fputs(" ],\n \"total\":[\n",jsonout); write_result(jsonout,"",&total,0); fputs(" ]\n}\n",jsonout);
if(fclose(jsonout)) io_error=1;
57 changes: 57 additions & 0 deletions research/f7-prefix-capacity-engine/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
# Opt-in matching capacity in the corrected word-census engine

**Scoped maintained-engine integration and bounded runtime decision; no new kappa.** This source-bound successor applies Ali Romman's PR5001 completion predicate inside Nick Petalas's maintained union-support census, which descends from Nicholas Stone's parity-corrected census. Frozen predecessor packages and receipts remain unchanged. The selected conditional `60403/20000000` is not a result of this task.

## Caller and change

The existing engine is not globally a simple-walk census: it admits repeated prefix vertices when the target Hamming-weight split permits them. Its exact target `S=T=L/2` is a simple-walk caller. At time `d`, a simple prefix has one distinct vertex at each time `0,...,d`. For a proposed nonclosing vertex at time `d+1`, the existing `ns + rem_even[d] >= S` and `nt + rem_odd[d] >= T` tests count every still-available position of the corresponding time parity. A repeated vertex fails its parity's inequality immediately, because it contributes no new distinct vertex while consuming one of the exactly `L/2` positions. By induction, every recursive prefix reached in this target split is simple. The final edge `q_L=0` is already handled separately and adds no prefix vertex.

`--prefix-capacity` requests the new predicate. It becomes active only for `N>=2`, even `4<=L<=2^N`, and `S=T=L/2`. Other target splits retain the original repeat-aware traversal with the predicate bypassed; JSON distinguishes requested and enabled. The optional predicate runs after the existing cheap multiplicity test and before extending the prefix. Each coordinate omission uses the actual classes of the functional with every coefficient one except the omitted coordinate, and accepts any final functional split admitted by PR5001. The Hamming-weight target split is never substituted for those functional splits. At `r=0` the predicate checks the closing edge directly; otherwise `crossing+r+1` includes that edge.

`vendor/union_census.c` is the exact existing engine at the pinned base, and `census.c` is its maintained successor entry point. `DELTA.diff` records every change. The default remains off; existing traversal, output file creation, shard/cap behavior, scientific report fields and hit format are retained. JSON adds requested/enabled status and a capacity-prune counter. The new source does not reinterpret the predecessor's `all_restored_leaves` or budget semantics.

## Exact evidence

`RESULT.json` records five complete small domains, each with all budgets disabled and with the unchanged default budgets. A temporary instrument at the real restored-leaf boundary compares full word `Counter`s for the pinned engine, successor off and successor on. Universal hit `Counter`s and scientific counts agree too. Default-off reports also agree in every non-timing predecessor field. The separately implemented firing census in `vendor/firing_census.c` supplies an independent complete simple restored-word multiset, filtered to the corrected engine's all-label scope. It is not used as a replacement engine or imported receipt.

| Domain | All restored leaves | Universal hits | No-budget nodes off / on | Default nodes off / on |
| --- | ---: | ---: | ---: | ---: |
| `n=2,L=4` | 1 | 1 | 5 / 5 | 5 / 5 |
| `n=3,L=6` | 4 | 4 | 16 / 16 | 16 / 16 |
| `n=4,L=8` | 27 | 22 | 91 / 91 | 81 / 81 |
| `n=4,L=10` | 110 | 110 | 566 / 534 | 566 / 534 |
| `n=5,L=12` | 3,381 | 828 | 17,360 / 16,765 | 8,401 / 8,278 |

The first PR5001 strict fixture, `010210`, omitted coordinate 0, remains rejected by the C kernel. In this actual engine it is already rejected by the earlier multiplicity/all-label test, illustrating why a theorem-level strict gain need not become an engine gain. The kernel agrees with PR5001's exact outer split set on all 436 prefix/omission pairs at `(4,8)`. Positive descendant completions reject three deliberate semantic mutations: the wrong omitted-coordinate functional (`010201`, omit 0), dropping the final edge from the crossing bound (`010201`, omit 1), and forcing a fixed half split (`010213`, omit 1). Both preserving and crossing closures pass. The source's unbalanced functional-completion control `0102132`, omit 1, lies in the checked prefix family. A repeat-capable weight target `(4,3)` retains all 18 restored leaves and bypasses capacity.

## Runtime decision

`TIMINGS.json` is local process-inclusive wall-time evidence: five samples per setting, fresh exclusive report/hit files, no leaf instrumentation, compilation excluded, no-budget complete searches. Samples were globally serialized on macOS 27.0.1 arm64, CPython 3.12.14, Apple clang 21.0.0, `-O2 -Wall -Wextra -Werror -std=c11`. The `(5,12)` median rose from **4.30 ms to 6.44 ms (1.50x)** despite 3.43% fewer nodes. The other medians are roughly 2–3 ms and dominated by process startup; their ratios do not establish a speedup. The bounded decision is to **retain opt-in status**. These short samples neither predict a seven-label production runtime nor justify another census.

## Reproduce

A C11 compiler supporting `unsigned __int128` and CPython 3.12 are required. The direct verifier needs no Git or network; the registered metadata checker uses repository history.

```sh
python3.12 -I -W error -B research/f7-prefix-capacity-engine/verify.py
python3.12 -I -W error -O -B research/f7-prefix-capacity-engine/verify.py
python3.12 -B scripts/research_package.py --package research/f7-prefix-capacity-engine --check-only
cc -O2 -Wall -Wextra -Werror -std=c11 -DN=5 -DL=12 research/f7-prefix-capacity-engine/census.c -o /tmp/census-capacity
# Choose new output paths; existing paths are never overwritten.
/tmp/census-capacity 6,6 --prefix-capacity --no-budgets --hits /tmp/new-capacity.hits --json /tmp/new-capacity.json
```

Expected direct marker: `PASS_F7_PREFIX_CAPACITY_ENGINE`. `--emit-receipt` prints regenerated deterministic evidence; ordinary replay compares it without modifying the receipt. `--timings` prints new local timing evidence, which is deliberately not a CI performance threshold. Each subprocess has an eight-second timeout and registered commands have a thirty-second bound. No seven-label run, full historical suite, Lean build, formal proof-kernel review or selected cold replay was performed.

The new check's observable contract is exact restored/accepted leaf multiplicity and report preservation at the real engine boundary. Credible regressions are an incorrect functional, omitted closing edge, or fixed-half substitution, each witnessed by a lost valid completion. PR5001's theorem tests do not exercise this engine or its split gate, so this package owns that integration boundary. Temporary instrumentation and a same-translation-unit kernel probe need no production export, injection option or test-only flag.

## Open next questions

1. Can an incrementally maintained version make the predicate worthwhile in a named larger simple-split shard? First profile the per-prefix work under a separately budgeted experiment; avoid default enablement from node reduction alone. No larger runtime evidence is supplied here.
2. A repeat-capable target cannot directly call PR5001. A different sound repeat-aware capacity theorem would be required before expanding the gate; the current implementation deliberately bypasses those calls.

## Sources and credit

Base: `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority revision 7. `SOURCES.json` pins the exact public bytes, paths and retained exports; PR5001 head `fe3226ea4e36469f43c6b116c5b98cc221a9b1af` is already an ancestor of this base. The union engine was introduced at `e09a08b5f85e648be373bece1b6ea1265d5ea8fa`; its unchanged source export preserves the full notices. The package's only external executable input is PR5001's `verify.py`, used only for its existing split function, not its historical traversal or proof replay.

Prepared for JoyboyBrian with substantial OpenAI Codex assistance. Credit: Ali Romman (PR5001/PR4992), Nick Petalas (PR4894 matching balance, union-support census), Mihir Srivastava (PR4907 handoff), Ross Richardson (PR943 singleton-prefix model), Nicholas Stone (PR2973 parity correction), Aaron Wang/opencode (retained word census), and Ryanson Jonathan with Claude Code assistance (independent firing census). New work and retained source are Apache-2.0. No independent human review, universal obstruction, complete multiplication theorem or new kappa is claimed.
Loading