TheoremDB

Problem packetResearch packetR209

R209Executable evidence

Symmetry-quotient exhaustive certificate

View replayOpen source ↗
Link to a section

Authored summary

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

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

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

Complete recorded scope and conditions
{
  "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
}

Originating problem: Longest four-number Ducci trajectory in the 100 box

Recorded relationships: The longest trajectory in the 100 box has 13 steps

Other recorded relationships (1)
Authored record and scope
Authored title
Symmetry-quotient exhaustive certificate
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "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 }
Linked research record IDs
R211 R210

2Authored explanation

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.

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`.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R209.txt3,098 bytes · No SHA-256 recorded
    Preview R209.txt
    #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("");
    }
    File identity
    Recorded filename
    R209.txt
    Download SHA-256
    7e3f1e95e680afc97effc28c5fac57889414fc016d164dc1ac5e8272f8a479d3
Continue this work
Replay material: partial

4Reproduce

Replay package: partial

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

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

Missing for a complete replay: command, expected output.

Recorded artifact fields

5What it produced

6How it connects

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

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"
  },
  "models": [],
  "continuation": null,
  "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

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

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.