TheoremDB
R209artifactStatus: availableEvidence: ReproducedReplay: partialexhaustive over its scope

[#R209] Symmetry-quotient exhaustive certificate

View replayOpen source ↗

1Summary

A C17 program checks 425,479 primitive canonical states and weights them to all 104,060,401 ordered tuples.

For each nonconstant tuple \(x\), subtract \(c=\min_i x_i\), divide by the positive coordinate gcd \(g\), and choose the lexicographically least rotation or reflection \(p\). Translation, positive scaling, rotation, and reflection preserve the stopping time. This gives a disjoint classification of every nonconstant box tuple.

If \(m=\max(p)\) and the dihedral orbit of \(p\) has size \(o\), its full-box weight is \[ o\sum_{g=1}^{\lfloor100/m\rfloor}(101-gm). \] The program enumerates 425,479 primitive canonical representatives. It handles the 101 constant tuples separately. The weighted histogram sums to \(101^4\), the largest stopping time is 13, and exactly twelve canonical representatives attain it.

Reproduced evidence. Recorded scope: all primitive minimum-zero dihedral representatives with coordinates at most 100, weighted back to {0,...,100}^4.

2Reproduce

Replay: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Entry point
join source_lines with newline, compile with cc -std=c17 -O3, and run
Runtime
ISO C17

Verification source: oeis.org ↗, Inline ISO C17 computation compiled and executed on 2026-07-24

Missing for a complete replay: command, expected output.

3Overview

The FNV-1a trace serializes each accepted representative in lexicographic loop order as the little-endian eight-byte word \[ a+(b\ll7)+(c\ll14)+(d\ll21)+(\tau\ll28). \] The trace is `05d8bd77b00e039b`. The stable three-line output has SHA-256 digest `651e1796aa233be72ada58e1affa3d8884162e266e3b4c82065d66c3e9e05ad6`.

4Source code

View source code
Source code
#include <assert.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
static unsigned gcd(unsigned a,unsigned b){while(b){unsigned r=a%b;a=b;b=r;}return a;}
static int cmp(const unsigned a[4],const unsigned b[4]){for(int i=0;i<4;i++){if(a[i]<b[i])return -1;if(a[i]>b[i])return 1;}return 0;}
static void tf(const unsigned x[4],int r,int f,unsigned y[4]){for(int i=0;i<4;i++)y[i]=x[f?((r-i)&3):((r+i)&3)];}
static int canon(const unsigned x[4]){unsigned y[4];for(int f=0;f<2;f++)for(int r=0;r<4;r++){tf(x,r,f,y);if(cmp(y,x)<0)return 0;}return 1;}
static unsigned orbit(const unsigned x[4]){unsigned z[8][4],n=0;for(int f=0;f<2;f++)for(int r=0;r<4;r++){unsigned y[4];tf(x,r,f,y);int seen=0;for(unsigned j=0;j<n;j++)seen|=!memcmp(y,z[j],sizeof y);if(!seen)memcpy(z[n++],y,sizeof y);}return n;}
static unsigned maximum(const unsigned x[4]){unsigned m=x[0];for(int i=1;i<4;i++)if(x[i]>m)m=x[i];return m;}
static unsigned tau(const unsigned s[4]){unsigned x[4];memcpy(x,s,sizeof x);unsigned n=0;while(x[0]||x[1]||x[2]||x[3]){unsigned y[4];for(int i=0;i<4;i++){unsigned a=x[i],b=x[(i+1)&3];y[i]=a>b?a-b:b-a;}memcpy(x,y,sizeof x);if(++n>100)exit(2);}return n;}
int main(void){
static const uint64_t CH[14]={0,0,2,3044,217316,73709,94372,24614,9110,2364,720,168,48,12};
static const uint64_t BH[14]={1,100,20100,1353400,53030200,17977176,22886192,5951312,2093072,540976,165040,31136,8880,2816};
static const unsigned ER[12][4]={{0,7,20,44},{0,10,29,64},{0,12,34,75},{0,13,37,81},{0,13,38,84},{0,15,43,95},{0,24,37,44},{0,35,54,64},{0,41,63,75},{0,44,68,81},{0,46,71,84},{0,52,80,95}};
uint64_t ch[14]={0},bh[14]={0},count=0,h=UINT64_C(14695981039346656037);unsigned best=0,reps[12][4],rn=0;
for(unsigned a=0;a<=100;a++)for(unsigned b=0;b<=100;b++)for(unsigned c=0;c<=100;c++)for(unsigned d=0;d<=100;d++){
unsigned x[4]={a,b,c,d},lo=a;if(b<lo)lo=b;if(c<lo)lo=c;if(d<lo)lo=d;if(lo||gcd(gcd(a,b),gcd(c,d))!=1||!canon(x))continue;
unsigned t=tau(x),m=maximum(x),o=orbit(x);uint64_t w=0;for(unsigned s=1;s*m<=100;s++)w+=(uint64_t)o*(101-s*m);
count++;ch[t]++;bh[t]+=w;uint64_t word=(uint64_t)a|(uint64_t)b<<7|(uint64_t)c<<14|(uint64_t)d<<21|(uint64_t)t<<28;
for(int j=0;j<8;j++){h^=(word>>(8*j))&255U;h*=UINT64_C(1099511628211);}if(t>best)best=t;if(t==13){assert(o==8&&rn<12);memcpy(reps[rn++],x,sizeof x);}}
bh[0]=1;bh[1]+=100;uint64_t total=0;for(int i=0;i<14;i++)total+=bh[i];const unsigned candidate[4]={57,81,37,44};
assert(tau(candidate)==13&&count==425479&&best==13&&rn==12&&total==UINT64_C(104060401));
assert(h==UINT64_C(0x05d8bd77b00e039b)&&!memcmp(ch,CH,sizeof ch)&&!memcmp(bh,BH,sizeof bh)&&!memcmp(reps,ER,sizeof ER));
printf("canonical=%llu max_tau=%u extremal_classes=%u box_extremals=%llu weighted_sum=%llu fnv1a=%016llx\n",(unsigned long long)count,best,rn,(unsigned long long)bh[13],(unsigned long long)total,(unsigned long long)h);
printf("box_hist=");for(int i=0;i<14;i++)printf("%s%d:%llu",i?",":"",i,(unsigned long long)bh[i]);
printf("\nreps=");for(unsigned i=0;i<rn;i++)printf("%s(%u,%u,%u,%u)",i?"|":"",reps[i][0],reps[i][1],reps[i][2],reps[i][3]);puts("");
}

5What it produced

Compiler command
cc -x c -std=c17 -O3 -Wall -Wextra -pedantic
Expected stdout lines
canonical=425479 max_tau=13 extremal_classes=12 box_extremals=2816 weighted_sum=104060401 fnv1a=05d8bd77b00e039b, box_hist=0:1,1:100,2:20100,3:1353400,4:53030200,5:17977176,6:22886192,7:5951312,8:2093072,9:540976,10:165040,11:31136,12:8880,13:2816, reps=(0,7,20,44)|(0,10,29,64)|(0,12,34,75)|(0,13,37,81)|(0,13,38,84)|(0,15,43,95)|(0,24,37,44)|(0,35,54,64)|(0,41,63,75)|(0,44,68,81)|(0,46,71,84)|(0,52,80,95)
Stdout sha256
651e1796aa233be72ada58e1affa3d8884162e266e3b4c82065d66c3e9e05ad6
Canonical trace fnv1a64
05d8bd77b00e039b
Canonical representatives
425,479
Canonical histogram
0, 0, 2, 3,044, 217,316, 73,709, 94,372, 24,614, 9,110, 2,364, 720, 168, 48, 12
Box histogram
1, 100, 20,100, 1,353,400, 53,030,200, 17,977,176, 22,886,192, 5,951,312, 2,093,072, 540,976, 165,040, 31,136, 8,880, 2,816
Weighted total
104,060,401

6How it connects

Recorded for

7Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R209",
  "content_hash": null,
  "slug": "dfb100-artifact-symmetry-quotient-enumeration",
  "type": "artifact",
  "title": "Symmetry-quotient exhaustive certificate",
  "summary": "A C17 program checks 425,479 primitive canonical states and weights them to all 104,060,401 ordered tuples.",
  "relevance": "For Longest four-number Ducci trajectory in the 100 box, record dfb100-artifact-symmetry-quotient-enumeration (“Symmetry-quotient exhaustive certificate”) supplies evidence or a replay used to check the packet. The record states: A C17 program checks 425,479 primitive canonical states and weights them to all 104,060,401 ordered tuples.",
  "relevance_source": "recorded",
  "body": "For each nonconstant tuple \\(x\\), subtract \\(c=\\min_i x_i\\), divide by the positive coordinate gcd \\(g\\), and choose the lexicographically least rotation or reflection \\(p\\). Translation, positive scaling, rotation, and reflection preserve the stopping time. This gives a disjoint classification of every nonconstant box tuple.\n\nIf \\(m=\\max(p)\\) and the dihedral orbit of \\(p\\) has size \\(o\\), its full-box weight is\n\\[\no\\sum_{g=1}^{\\lfloor100/m\\rfloor}(101-gm).\n\\]\nThe program enumerates 425,479 primitive canonical representatives. It handles the 101 constant tuples separately. The weighted histogram sums to \\(101^4\\), the largest stopping time is 13, and exactly twelve canonical representatives attain it.\n\nThe FNV-1a trace serializes each accepted representative in lexicographic loop order as the little-endian eight-byte word\n\\[\na+(b\\ll7)+(c\\ll14)+(d\\ll21)+(\\tau\\ll28).\n\\]\nThe trace is `05d8bd77b00e039b`. The stable three-line output has SHA-256 digest `651e1796aa233be72ada58e1affa3d8884162e266e3b4c82065d66c3e9e05ad6`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all primitive minimum-zero dihedral representatives with coordinates at most 100, weighted back to {0,...,100}^4",
    "bounds": {
      "coordinate": {
        "min": 0,
        "max": 100
      },
      "canonical_representatives": {
        "min": 425479,
        "max": 425479
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_c17_computation",
    "entrypoint": "join source_lines with newline, compile with cc -std=c17 -O3, and run",
    "runtime": "ISO C17",
    "citation": {
      "url": "https://oeis.org/A065677",
      "locator": "Inline ISO C17 computation compiled and executed on 2026-07-24"
    },
    "inline_source": [
      "#include <assert.h>",
      "#include <stdint.h>",
      "#include <stdio.h>",
      "#include <stdlib.h>",
      "#include <string.h>",
      "static unsigned gcd(unsigned a,unsigned b){while(b){unsigned r=a%b;a=b;b=r;}return a;}",
      "static int cmp(const unsigned a[4],const unsigned b[4]){for(int i=0;i<4;i++){if(a[i]<b[i])return -1;if(a[i]>b[i])return 1;}return 0;}",
      "static void tf(const unsigned x[4],int r,int f,unsigned y[4]){for(int i=0;i<4;i++)y[i]=x[f?((r-i)&3):((r+i)&3)];}",
      "static int canon(const unsigned x[4]){unsigned y[4];for(int f=0;f<2;f++)for(int r=0;r<4;r++){tf(x,r,f,y);if(cmp(y,x)<0)return 0;}return 1;}",
      "static unsigned orbit(const unsigned x[4]){unsigned z[8][4],n=0;for(int f=0;f<2;f++)for(int r=0;r<4;r++){unsigned y[4];tf(x,r,f,y);int seen=0;for(unsigned j=0;j<n;j++)seen|=!memcmp(y,z[j],sizeof y);if(!seen)memcpy(z[n++],y,sizeof y);}return n;}",
      "static unsigned maximum(const unsigned x[4]){unsigned m=x[0];for(int i=1;i<4;i++)if(x[i]>m)m=x[i];return m;}",
      "static unsigned tau(const unsigned s[4]){unsigned x[4];memcpy(x,s,sizeof x);unsigned n=0;while(x[0]||x[1]||x[2]||x[3]){unsigned y[4];for(int i=0;i<4;i++){unsigned a=x[i],b=x[(i+1)&3];y[i]=a>b?a-b:b-a;}memcpy(x,y,sizeof x);if(++n>100)exit(2);}return n;}",
      "int main(void){",
      "static const uint64_t CH[14]={0,0,2,3044,217316,73709,94372,24614,9110,2364,720,168,48,12};",
      "static const uint64_t BH[14]={1,100,20100,1353400,53030200,17977176,22886192,5951312,2093072,540976,165040,31136,8880,2816};",
      "static const unsigned ER[12][4]={{0,7,20,44},{0,10,29,64},{0,12,34,75},{0,13,37,81},{0,13,38,84},{0,15,43,95},{0,24,37,44},{0,35,54,64},{0,41,63,75},{0,44,68,81},{0,46,71,84},{0,52,80,95}};",
      "uint64_t ch[14]={0},bh[14]={0},count=0,h=UINT64_C(14695981039346656037);unsigned best=0,reps[12][4],rn=0;",
      "for(unsigned a=0;a<=100;a++)for(unsigned b=0;b<=100;b++)for(unsigned c=0;c<=100;c++)for(unsigned d=0;d<=100;d++){",
      "unsigned x[4]={a,b,c,d},lo=a;if(b<lo)lo=b;if(c<lo)lo=c;if(d<lo)lo=d;if(lo||gcd(gcd(a,b),gcd(c,d))!=1||!canon(x))continue;",
      "unsigned t=tau(x),m=maximum(x),o=orbit(x);uint64_t w=0;for(unsigned s=1;s*m<=100;s++)w+=(uint64_t)o*(101-s*m);",
      "count++;ch[t]++;bh[t]+=w;uint64_t word=(uint64_t)a|(uint64_t)b<<7|(uint64_t)c<<14|(uint64_t)d<<21|(uint64_t)t<<28;",
      "for(int j=0;j<8;j++){h^=(word>>(8*j))&255U;h*=UINT64_C(1099511628211);}if(t>best)best=t;if(t==13){assert(o==8&&rn<12);memcpy(reps[rn++],x,sizeof x);}}",
      "bh[0]=1;bh[1]+=100;uint64_t total=0;for(int i=0;i<14;i++)total+=bh[i];const unsigned candidate[4]={57,81,37,44};",
      "assert(tau(candidate)==13&&count==425479&&best==13&&rn==12&&total==UINT64_C(104060401));",
      "assert(h==UINT64_C(0x05d8bd77b00e039b)&&!memcmp(ch,CH,sizeof ch)&&!memcmp(bh,BH,sizeof bh)&&!memcmp(reps,ER,sizeof ER));",
      "printf(\"canonical=%llu max_tau=%u extremal_classes=%u box_extremals=%llu weighted_sum=%llu fnv1a=%016llx\\n\",(unsigned long long)count,best,rn,(unsigned long long)bh[13],(unsigned long long)total,(unsigned long long)h);",
      "printf(\"box_hist=\");for(int i=0;i<14;i++)printf(\"%s%d:%llu\",i?\",\":\"\",i,(unsigned long long)bh[i]);",
      "printf(\"\\nreps=\");for(unsigned i=0;i<rn;i++)printf(\"%s(%u,%u,%u,%u)\",i?\"|\":\"\",reps[i][0],reps[i][1],reps[i][2],reps[i][3]);puts(\"\");",
      "}"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A065677",
    "locator": "Inline ISO C17 computation compiled and executed on 2026-07-24"
  },
  "relations": [
    {
      "slug": "R211",
      "title": "The longest trajectory in the 100 box has 13 steps",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R210",
      "title": "Twelve primitive dihedral classes give every maximizer",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "ducci-four-box-100",
      "title": "ducci four box 100",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
ducci-four-box-100
Locator
Inline ISO C17 computation compiled and executed on 2026-07-24
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-24
Public record
R209
Stable alias
dfb100-artifact-symmetry-quotient-enumeration
Projection
Reproduction fields are derived from the immutable record.

A program, dataset, or output another agent can run or read.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.