pith:V2F6FVEA
The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
A mechanized theorem proves that a fixed step-duplicating recursor lies outside all named direct termination measure classes.
arxiv:2512.00081 v10 · 2025-11-26 · cs.LO · math.LO
Add to your LaTeX paper
\usepackage{pith}
\pithnumber{V2F6FVEAMO3J6DX7FROIPU6UYV}
Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge
Record completeness
Claims
We formalize the orientation boundary for first-order step-duplicating recursors: a mechanized object-level barrier theorem, proved without reductions or undecidability, showing that a fixed terminating recursor lies outside named direct termination-measure classes.
The twelve base measure classes (additive, transparency-constrained compositional, scalar growth families, tracked vector and pair families) together with the arctic/tropical extensions and scalar-dominance data exhaust the relevant direct termination measures for the recursor in question.
Lean 4 formalization establishes an object-level orientation boundary showing fixed step-duplicating recursors lie outside explicit direct termination-measure classes, with three escape routes and tool connections.
Formal links
Receipt and verification
| First computed | 2026-05-22T01:03:51.384121Z |
|---|---|
| Builder | pith-number-builder-2026-05-17-v1 |
| Signature | Pith Ed25519
(pith-v1-2026-05) · public key |
| Schema | pith-number/v1.0 |
Canonical hash
ae8be2d48063b69f0eff2c5c87d3d4c54aa31b55367959b0ffdaa3af1f439d09
Aliases
· · · · ·Agent API
Verify this Pith Number yourself
curl -sH 'Accept: application/ld+json' https://pith.science/pith/V2F6FVEAMO3J6DX7FROIPU6UYV \
| jq -c '.canonical_record' \
| python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: ae8be2d48063b69f0eff2c5c87d3d4c54aa31b55367959b0ffdaa3af1f439d09
Canonical record JSON
{
"metadata": {
"abstract_canon_sha256": "674c705d1b0b391475396cfbb17af5cf07c5d51709dd71be75b0d101425b407e",
"cross_cats_sorted": [
"math.LO"
],
"license": "http://creativecommons.org/licenses/by-nc-nd/4.0/",
"primary_cat": "cs.LO",
"submitted_at": "2025-11-26T00:50:17Z",
"title_canon_sha256": "5425051c777fdf576fae9f18a5996e2e72817cf984b15de85b4e9316dbb495a9"
},
"schema_version": "1.0",
"source": {
"id": "2512.00081",
"kind": "arxiv",
"version": 10
}
}