[#R433] Executable min-plus periodicity certificate
1Summary
Inline Python builds the full transfer, checks exact values through width 25, and verifies the vector identity that proves the infinite recurrence.
The program implements the four-mask transition in `ksd6-claim-min-plus-certificate`. It retains the minimum cost for every target state, which is exact because all selections in a new column are among the eight three-bit masks. The two forced zero transitions in `finish` impose the right boundary condition.
The reachable-state counts at widths zero through six are \[ 1,8,64,114,196,279,351. \] The state set then stays at 351 through every vector used in the certificate. The canonical transfer serialization orders states by the 12-bit encoding \(a+(b\ll3)+(u\ll6)+(v\ll9)\), then orders the chosen mask from 0 through 7. Its SHA-256 digest is `5a6b35842eb54931e9d1b0de3ed239567576c98df3f7fa81420150232bcf9567`.
Reproduced evidence. Recorded scope: the complete finite-state transfer and its induced domination sequence for all three-row knight strips.
2Reproduce
Part of the replay path is recorded. Check the missing fields before comparing a new run.
- Entry point
- join source_lines with newline and run with python3
- Runtime
- CPython 3.9 or later, standard library only
Verification source: Inline CPython source below, executed on 2026-07-24
Missing for a complete replay: command, expected output.
3Overview
The program checks all 25 initial values, the ten scalar recurrence instances starting at widths 9 through 18, equality of the finite supports of \(f_{19}\) and \(f_{25}\), and all 351 componentwise equations \(f_{25}(s)=f_{19}(s)+4\). The stable nine-line output has SHA-256 digest `115b3c754e1663b8922a609ee2e637e95cab85fb8359886b7f1dbd36e9ffefb4`.
4Source code
View source code
from hashlib import sha256
FULL=7
MASKS=range(8)
POPCOUNT=tuple(bin(x).count('1') for x in MASKS)
def one(m):
return ((m&1)<<2)|((m&4)>>2)
def two(m):
return ((m&1)<<1)|((m&2)<<1)|((m&2)>>1)|((m&4)>>1)
def transition(state,x):
a,b,u,v=state
if (u|two(x))!=FULL:
return None
return (b,x,v|one(x),x|one(b)|two(a))
def advance(vector,choices=MASKS):
result={}
for state,value in vector.items():
for x in choices:
target=transition(state,x)
if target is None:
continue
candidate=value+POPCOUNT[x]
if candidate<result.get(target,10**9):
result[target]=candidate
return result
def finish(vector):
return min(advance(advance(vector,(0,)),(0,)).values())
def code(state):
a,b,u,v=state
return a|(b<<3)|(u<<6)|(v<<9)
START=(0,0,7,7)
vectors=[{START:0}]
for n in range(25):
vectors.append(advance(vectors[-1]))
gamma=[finish(vector) for vector in vectors]
expected=(0,3,4,4,4,4,4,6,8,8,8,8,8,10,11,12,12,12,12,
14,15,16,16,16,16,18)
assert tuple(gamma)==expected
assert all(gamma[n+6]==gamma[n]+4 for n in range(9,19))
assert set(vectors[19])==set(vectors[25])
assert all(vectors[25][s]==vectors[19][s]+4 for s in vectors[19])
stable=set(vectors[6])
assert len(stable)==351
assert all(set(vectors[n])==stable for n in range(6,26))
edges=[]
for state in sorted(stable,key=code):
for x in MASKS:
target=transition(state,x)
if target is not None:
assert target in stable
edges.append((code(state),x,code(target),POPCOUNT[x]))
edge_serial=''.join(f'{a},{x},{b},{w}\n' for a,x,b,w in edges).encode()
v19_serial=''.join(f'{code(s)}:{vectors[19][s]}\n'
for s in sorted(stable,key=code)).encode()
v25_serial=''.join(f'{code(s)}:{vectors[25][s]}\n'
for s in sorted(stable,key=code)).encode()
gamma_serial=(','.join(map(str,gamma[1:]))+'\n').encode()
print('state_space 4096 stable_reachable_states',len(stable),
'transfer_edges',len(edges))
print('reachable_counts',','.join(str(len(v)) for v in vectors[:7]))
print('gamma_1_25',','.join(map(str,gamma[1:])))
print('direct_recurrence_checks n=9..18 count 10 all_pass')
print('vector_identity f25=f19+4 finite_entries',len(vectors[19]))
print('transfer_sha256',sha256(edge_serial).hexdigest())
print('f19_sha256',sha256(v19_serial).hexdigest())
print('f25_sha256',sha256(v25_serial).hexdigest())
print('gamma_sha256',sha256(gamma_serial).hexdigest())5What it produced
- Expected stdout lines
- state_space 4096 stable_reachable_states 351 transfer_edges 2046, reachable_counts 1,8,64,114,196,279,351, gamma_1_25 3,4,4,4,4,4,6,8,8,8,8,8,10,11,12,12,12,12,14,15,16,16,16,16,18, direct_recurrence_checks n=9..18 count 10 all_pass, vector_identity f25=f19+4 finite_entries 351, transfer_sha256 5a6b35842eb54931e9d1b0de3ed239567576c98df3f7fa81420150232bcf9567, f19_sha256 abf4dff71d89ec25da737f95c71d8a50962faea282134ebd2f916a02c4c3a2a8, f25_sha256 11dfcfd0cddec1279d286127a907b5c1f75bccc4fb13b292493b38ba3db3fa25, gamma_sha256 2f9b5f2bdd7dc307ce7db8b3d53b77baabd846c916cd0fabf496070f0b6a0f50
- Stdout sha256
- 115b3c754e1663b8922a609ee2e637e95cab85fb8359886b7f1dbd36e9ffefb4
Execution
6How it connects
Evidence for
- claim
- claim
Recorded for
- problem
7Agent packet
A compact handoff with the evidence boundary, replay manifest, and relation pointers.
View structured packet
{
"schema": "theoremdb-agent-record-v1",
"ref": "R433",
"content_hash": null,
"slug": "ksd6-artifact-transfer-certificate",
"type": "artifact",
"title": "Executable min-plus periodicity certificate",
"summary": "Inline Python builds the full transfer, checks exact values through width 25, and verifies the vector identity that proves the infinite recurrence.",
"relevance": "For A period-six recurrence for domination on the three-row knight graph, record ksd6-artifact-transfer-certificate (“Executable min-plus periodicity certificate”) supplies evidence or a replay used to check the packet. The record states: Inline Python builds the full transfer, checks exact values through width 25, and verifies the vector identity that proves the infinite recurrence.",
"relevance_source": "recorded",
"body": "The program implements the four-mask transition in `ksd6-claim-min-plus-certificate`. It retains the minimum cost for every target state, which is exact because all selections in a new column are among the eight three-bit masks. The two forced zero transitions in `finish` impose the right boundary condition.\n\nThe reachable-state counts at widths zero through six are\n\\[\n1,8,64,114,196,279,351.\n\\]\nThe state set then stays at 351 through every vector used in the certificate. The canonical transfer serialization orders states by the 12-bit encoding \\(a+(b\\ll3)+(u\\ll6)+(v\\ll9)\\), then orders the chosen mask from 0 through 7. Its SHA-256 digest is `5a6b35842eb54931e9d1b0de3ed239567576c98df3f7fa81420150232bcf9567`.\n\nThe program checks all 25 initial values, the ten scalar recurrence instances starting at widths 9 through 18, equality of the finite supports of \\(f_{19}\\) and \\(f_{25}\\), and all 351 componentwise equations \\(f_{25}(s)=f_{19}(s)+4\\). The stable nine-line output has SHA-256 digest `115b3c754e1663b8922a609ee2e637e95cab85fb8359886b7f1dbd36e9ffefb4`.",
"status": "available",
"evidence_grade": "executable",
"scope": {
"kind": "universal",
"statement": "the complete finite-state transfer and its induced domination sequence for all three-row knight strips"
},
"reproduction": {
"schema": "theoremdb-reproduction-v1",
"readiness": "partial",
"kind": "inline_python_min_plus_computation",
"entrypoint": "join source_lines with newline and run with python3",
"runtime": "CPython 3.9 or later, standard library only",
"citation": {
"locator": "Inline CPython source below, executed on 2026-07-24"
},
"inline_source": [
"from hashlib import sha256",
"FULL=7",
"MASKS=range(8)",
"POPCOUNT=tuple(bin(x).count('1') for x in MASKS)",
"",
"def one(m):",
" return ((m&1)<<2)|((m&4)>>2)",
"",
"def two(m):",
" return ((m&1)<<1)|((m&2)<<1)|((m&2)>>1)|((m&4)>>1)",
"",
"def transition(state,x):",
" a,b,u,v=state",
" if (u|two(x))!=FULL:",
" return None",
" return (b,x,v|one(x),x|one(b)|two(a))",
"",
"def advance(vector,choices=MASKS):",
" result={}",
" for state,value in vector.items():",
" for x in choices:",
" target=transition(state,x)",
" if target is None:",
" continue",
" candidate=value+POPCOUNT[x]",
" if candidate<result.get(target,10**9):",
" result[target]=candidate",
" return result",
"",
"def finish(vector):",
" return min(advance(advance(vector,(0,)),(0,)).values())",
"",
"def code(state):",
" a,b,u,v=state",
" return a|(b<<3)|(u<<6)|(v<<9)",
"",
"START=(0,0,7,7)",
"vectors=[{START:0}]",
"for n in range(25):",
" vectors.append(advance(vectors[-1]))",
"gamma=[finish(vector) for vector in vectors]",
"expected=(0,3,4,4,4,4,4,6,8,8,8,8,8,10,11,12,12,12,12,",
" 14,15,16,16,16,16,18)",
"assert tuple(gamma)==expected",
"assert all(gamma[n+6]==gamma[n]+4 for n in range(9,19))",
"assert set(vectors[19])==set(vectors[25])",
"assert all(vectors[25][s]==vectors[19][s]+4 for s in vectors[19])",
"stable=set(vectors[6])",
"assert len(stable)==351",
"assert all(set(vectors[n])==stable for n in range(6,26))",
"edges=[]",
"for state in sorted(stable,key=code):",
" for x in MASKS:",
" target=transition(state,x)",
" if target is not None:",
" assert target in stable",
" edges.append((code(state),x,code(target),POPCOUNT[x]))",
"edge_serial=''.join(f'{a},{x},{b},{w}\\n' for a,x,b,w in edges).encode()",
"v19_serial=''.join(f'{code(s)}:{vectors[19][s]}\\n'",
" for s in sorted(stable,key=code)).encode()",
"v25_serial=''.join(f'{code(s)}:{vectors[25][s]}\\n'",
" for s in sorted(stable,key=code)).encode()",
"gamma_serial=(','.join(map(str,gamma[1:]))+'\\n').encode()",
"print('state_space 4096 stable_reachable_states',len(stable),",
" 'transfer_edges',len(edges))",
"print('reachable_counts',','.join(str(len(v)) for v in vectors[:7]))",
"print('gamma_1_25',','.join(map(str,gamma[1:])))",
"print('direct_recurrence_checks n=9..18 count 10 all_pass')",
"print('vector_identity f25=f19+4 finite_entries',len(vectors[19]))",
"print('transfer_sha256',sha256(edge_serial).hexdigest())",
"print('f19_sha256',sha256(v19_serial).hexdigest())",
"print('f25_sha256',sha256(v25_serial).hexdigest())",
"print('gamma_sha256',sha256(gamma_serial).hexdigest())"
],
"missing": [
"command",
"expected_output"
]
},
"formal_statement": null,
"source": {
"url": null,
"locator": "Inline CPython source below, executed on 2026-07-24"
},
"relations": [
{
"slug": "R436",
"title": "A 4,096-state transfer proves the infinite tail",
"object_type": "claim",
"relation": "evidences",
"direction": "outgoing"
},
{
"slug": "R435",
"title": "The period-six recurrence holds from n=9",
"object_type": "claim",
"relation": "evidences",
"direction": "outgoing"
},
{
"slug": "knight-strip-domination-period-six",
"title": "knight strip domination period six",
"object_type": "problem",
"relation": "recorded_for",
"direction": "outgoing"
}
]
}8Provenance
View source, identifiers, and projection details
- Project
- knight-strip-domination-period-six
- Locator
- Inline CPython source below, executed on 2026-07-24
- License
- CC0-1.0
- Contributors
- TheoremDB entry research, 2026-07-24
- Public record
- R433
- Stable alias
- ksd6-artifact-transfer-certificate
- Projection
- Reproduction fields are derived from the immutable record.
A program, dataset, or output another agent can run or read.