From 39f9c29448f92711ef2c6436b70916935dc96eee Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Fri, 23 Oct 2026 02:22:00 -0700
Subject: [PATCH 1/2] Execute complete CRT repair source control with static
 key return and CFG bound

---
 research/crt-complete-repair-control/PROOF.md | 151 +++++++++++++++
 .../crt-complete-repair-control/compiler.py   | 179 ++++++++++++++++++
 .../crt-complete-repair-control/machine.py    | 137 ++++++++++++++
 3 files changed, 467 insertions(+)
 create mode 100644 research/crt-complete-repair-control/PROOF.md
 create mode 100644 research/crt-complete-repair-control/compiler.py
 create mode 100644 research/crt-complete-repair-control/machine.py

diff --git a/research/crt-complete-repair-control/PROOF.md b/research/crt-complete-repair-control/PROOF.md
new file mode 100644
index 0000000000..d5e56adbe7
--- /dev/null
+++ b/research/crt-complete-repair-control/PROOF.md
@@ -0,0 +1,151 @@
+# Complete outer control at the actual fixed CRT repair port
+
+## Statement
+
+This is a fixed-geometry finite-symbol program theorem, not an all-size CRT
+or multiplication theorem. Let the six borrowed unary records G,H,K,Y,J,B
+encode (2,2,6,8,2,0), using the retained `< 1^n >` representation with blank
+tail. Let the borrowed ROM be `L F R`, where F is any32-bit Boolean table
+satisfying F[v]=F[v xor4]. Let data contain4096 opaque symbols from the fixed
+alphabet {('R',v):0<=v<4096}, framed by `<` and `>`. The data is the raw
+post-S stream for the retained ten-shear compact map S, with source
+f(y)=F[y mod32]. All roles are physically distinct, heads initially zero,
+all owned roles are initially blank. The program installs each outer `<`
+marker through a charged write, then erases it after the source cleanup. Arbitrary finite blank tails are allowed.
+
+The fixed program returned by `assemble` has no runtime instance parameters.
+It returns data in the ideal T-image order; it preserves the six unary
+records and ROM, erases every consumed/private role, returns every tape
+head, and resets every finite-control register. Each of the2944 bad addresses
+calls the actual key exactly once; good addresses never do. It is a theorem
+for arbitrary payloads in that fixed alphabet and every admitted ROM, not
+an inference from the one canonical numerical fixture.
+
+Raw S preparation and ROM construction are input contracts. This work does
+not execute S, its twelve paid shuttles, a descriptor/ROM producer, a larger
+geometry key, or a complete E(p,ell) evaluator. A marked-role input adapter
+allocates fixed blank owned roles; it does not initialize arbitrary borrowed
+dirty storage. Rejecting malformed executions have no rollback guarantee.
+
+## Source refinement and static compilation
+
+The retained #4208 producer, #4201 scanner and #4637 bridge contain finite
+symbol tests and marker-driven loops, but execute them as Python control.
+#4795 implements the key as explicit instructions while the outer caller
+still has only a cell-action invoice. This package compiles those unchanged
+source ASTs at assembly time and runs none of their Python functions during
+execution. Source hashes are authenticated before assembly.
+
+Each source local has a private finite register at each static inline call
+site. Mutable parameters are copied before entry, preserving call-by-value
+binding while tape-role values still refer to the same physical tape. Locals
+are allocated before compiling conditions or either arm; loop tests and both
+arms therefore name the same assigned register. Source calls are expanded
+statically and recursive source calls are rejected. Each return jumps to a
+static continuation. The key instructions are inserted with relocated static
+PCs, a disjoint register namespace, and a fixed map for counter/stream/ROM
+and its twelve private roles. Its accepting halt becomes a jump to the
+unique split continuation. No runtime call stack or callable exists.
+
+A source assignment becomes a finite-register copy. Comparisons, negation,
+fixed tuple fields and fixed tuples become finite truth-table operations.
+Short-circuit Boolean expressions and conditional expressions become branch
+and copy sequences, preserving both evaluation order and tape-read side
+effects. `while` becomes a static back edge with its test reevaluated each
+time; `break` and `return` become patched static jumps. `for` is accepted only
+on a statically bounded tuple, expanded at assembly time. No data-dependent
+range or numeric induction variable is admitted. Tape.read/write/move become
+single-cell instructions, with move restricted to +/-1. A tape-role register
+ranges over the fixed finite bank; choosing a role is a finite multiplexer,
+not an encoded address into data. Field projections have compile-time indices.
+
+The source record predicate is implemented on the declared finite4096-symbol
+record alphabet. The tuple representation in the emulator is a symbol name;
+its numeric payload never becomes a machine address, arithmetic operand or
+loop bound. Stencil atoms form a fixed finite product alphabet too. This is
+not a literal binary transition table or a unit-price unbounded tuple machine:
+all tuple arities, fields, role values and alphabets are bounded independently
+of the input payloads. A binary encoding and its constants remain unclaimed.
+
+Valid executions of the source producer do not take its exception handlers.
+The compiler deliberately maps all raises to rejecting halts, preserving the
+stated successful-domain theorem while making no source exception-cleanup
+or transactional-rejection equivalence claim. Static mutation flags are
+specialized to the normal program. Instrumentation callbacks/meters are
+removed during assembly; the unpaid evaluate_key is replaced by the entire
+literal key program, not by a host result. A verifier observer can inspect
+states but its values never enter execution.
+
+Induction on the supported expressions/statements gives equality of tape
+operations and finite source state at statement boundaries. Loop induction
+then lifts this relation through the retained source algorithms. The inherited
+producer/scanner proof gives the actual owned stencil and mask; the retained
+key theorem gives T(S^-1(q)) from the current counter and ROM; the bridge's
+split/radix/reinsert proof gives the ideal payload endpoint and exact bad-only
+call set. The source ownership proof, the key's cleanup, and the explicit
+control initialization/final reset establish the full successful boundary.
+
+## Complete instruction ledger
+
+Every executed read, write, one-cell move, finite-symbol operation, branch,
+jump and halt costs one. Initial register writes, outer-marker installation/disposal and final reset
+are explicit instructions. The executor's heads, PC, step totals and event observations
+are configuration/observer machinery, never program operands.
+
+Cut outgoing CFG edges at each read/write/move (and halt). The checker rejects
+any cycle in the remaining graph and computes its longest path length D by
+a topological pass. Thus between successive charged cell actions, before the
+first and after the last, the machine executes at most D instructions. For
+any finite execution with C cell actions,
+
+    T <= (D+1)(C+1).
+
+The extra1 is deliberately conservative about whether the ending cell action
+is included. This argument covers every possible branch, including branches
+not taken by the calibration; the observed maximum alone is not the proof.
+A control-only-cycle mutation must be rejected.
+
+For a parameter-only bound in this fixed geometry, write M=4096,L=12,N=2944.
+Exclude all inlined-key actions from the outer cell count. Counter setup has
+at most10(L+1) actions. Each split/address-carry iteration has at most
+20(L+1) actions. A radix pass, including last-bit search, key rotation, both
+bucket rewinds, concatenation and erasure, has at most100N(L+1)+100 actions;
+there are L passes. Reinsertion/counter checking has at most40M(L+1) actions.
+Final erasure traverses at most a constant ten times the total
+M+N(L+1)+L+10 retained cells. These estimates follow by counting the reads,
+writes and one-cell moves in each unchanged source loop; no loop scans past
+its marker. The22 outer-marker lifecycle writes are additional. Producer841 and scanner454830 are exact on the declared unary
+geometry. Summing these charges is less than
+
+    C_outer <= 1000 M (L+1)^2.
+
+The retained key theorem gives T_key<=3,287,110, hence also C_key<=3,287,110,
+for each admitted q,F. All actual key operations, including its append port,
+are counted there; the removed host interface must not be added again. Thus
+
+    C <= 1000 M (L+1)^2 + N*3,287,110,
+    T <= (D+1)*(1000 M (L+1)^2 + N*3,287,110 +1).
+
+This loose bound closes the finite-symbol instruction ledger; it neither
+improves the source asymptotic tariff nor proves full E absorption. Exact
+observed counts are separately frozen in RESULT.json. Physical storage is
+bounded by the fixed source roles: two record buckets each N(L+1)+2,
+keyed bad N(L+1)+2, good M-N+2, data M+2, mask M+2, stencil/counter L+2,
+the eight finite unary work extents and key roles. Reusing four emptied
+producer roles for good/bad/buckets is included; no live role is aliased.
+Finite-control register storage is fixed and separately reset.
+
+## Evidence and remaining questions
+
+The actual canonical middle-layer fixture comes from h3, modulus5,
+offsets[0,2,4,0]. Host arrays only construct declared raw-S/ROM inputs and
+independent expected output; they do not supply the machine's mask, keys,
+branches or traversals. The independent observer checks each current key
+counter, exact returned key, scratch erasure and final caller ownership.
+Finite tests corroborate the written refinement; they are not independent
+human or proof-kernel acceptance.
+
+Open: binary lowering of this complete alphabet; variable-geometry key
+control; actual raw macro with twelve dirty-back shuttles; descriptor/ROM
+production in the same lifecycle; full evaluator/native/precision/outer
+admission. No selected frontier or new kappa is claimed.
diff --git a/research/crt-complete-repair-control/compiler.py b/research/crt-complete-repair-control/compiler.py
new file mode 100644
index 0000000000..e0004e1c2f
--- /dev/null
+++ b/research/crt-complete-repair-control/compiler.py
@@ -0,0 +1,179 @@
+"""Static AST lowering of the retained finite-control source, not a runtime evaluator.
+
+JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+No runtime Python function, AST, numeric loop bound or source callable survives.
+"""
+import ast
+
+C=lambda x:('c',x)
+R=lambda x:('r',x)
+
+class Compiler:
+    def __init__(self,sources,key):
+        self.functions={}
+        for ns,text in sources.items():
+            tree=ast.parse(text)
+            self.functions[ns]={n.name:n for n in tree.body if isinstance(n,ast.FunctionDef)}
+        self.code=[];self.serial=0;self.roles=[];self.key=key;self.calls=[];self.key_sites=[]
+        self.globals={'LEFT':C('<'),'END':C('>'),'BLANK':C('_'),'SKIP':C(('S',False,False,'0','0'))}
+    def fresh(self):self.serial+=1;return 'v'+str(self.serial)
+    def emit(self,*a):self.code.append(a);return len(self.code)-1
+    def patch(self,i,*a):self.code[i]=a
+    def value(self,expr,env,ns):
+        if isinstance(expr,ast.Constant):return C(expr.value)
+        if isinstance(expr,ast.Name):return env.get(expr.id,self.globals.get(expr.id)) or self.fail(expr)
+        if isinstance(expr,ast.Tuple):return ('tuple',tuple(self.value(x,env,ns) for x in expr.elts))
+        if isinstance(expr,ast.UnaryOp):
+            a=self.value(expr.operand,env,ns)
+            if isinstance(expr.op,ast.USub) and a[0]=='c':return C(-a[1])
+            if isinstance(expr.op,ast.Not):
+                if a[0]=='c':return C(not a[1])
+                z=R(self.fresh());self.emit('not',a,z[1]);return z
+        if isinstance(expr,ast.Compare):
+            if len(expr.ops)!=1:raise ValueError('chained compare')
+            a=self.value(expr.left,env,ns);b=self.value(expr.comparators[0],env,ns)
+            op={ast.Eq:'eq',ast.NotEq:'ne',ast.Is:'eq',ast.IsNot:'ne',ast.In:'in',ast.NotIn:'notin'}[type(expr.ops[0])]
+            if a[0]=='c' and b[0]=='c':return C(self.compare(op,a[1],b[1]))
+            z=R(self.fresh());self.emit(op,a,b,z[1]);return z
+        if isinstance(expr,ast.BoolOp):
+            z=R(self.fresh());ends=[]
+            for i,x in enumerate(expr.values):
+                a=self.value(x,env,ns);self.emit('copy',a,z[1])
+                if i+1<len(expr.values):
+                    j=self.emit('branch',z,None,None);ends.append(j)
+                    self.patch(j,'branch',z,len(self.code) if isinstance(expr.op,ast.And) else None,None if isinstance(expr.op,ast.And) else len(self.code))
+            end=len(self.code)
+            for j in ends:
+                op,a,t,f=self.code[j];self.patch(j,op,a,end if t is None else t,end if f is None else f)
+            return z
+        if isinstance(expr,ast.IfExp):
+            test=self.value(expr.test,env,ns)
+            if test[0]=='c':return self.value(expr.body if test[1] else expr.orelse,env,ns)
+            z=R(self.fresh());j=self.emit('branch',test,None,None);start=len(self.code)
+            a=self.value(expr.body,env,ns);self.emit('copy',a,z[1]);end=self.emit('jump',None);other=len(self.code)
+            b=self.value(expr.orelse,env,ns);self.emit('copy',b,z[1]);self.patch(j,'branch',test,start,other);self.patch(end,'jump',len(self.code));return z
+        if isinstance(expr,ast.Subscript):
+            a=self.value(expr.value,env,ns);i=ast.literal_eval(expr.slice)
+            if not isinstance(i,int) or i<0:raise ValueError('fixed field projection only')
+            if a[0]=='tuple':return a[1][i]
+            z=R(self.fresh());self.emit('field',a,i,z[1]);return z
+        if isinstance(expr,ast.Call):
+            if isinstance(expr.func,ast.Attribute):
+                role=self.value(expr.func.value,env,ns);op=expr.func.attr
+                if expr.keywords or len(expr.args)!=(0 if op=='read' else 1):raise ValueError('method arity')
+                if op=='read':
+                    z=R(self.fresh());self.emit('read',role,z[1]);return z
+                if op in ('write','move'):
+                    a=self.value(expr.args[0],env,ns)
+                    if op=='move' and (a[0]!='c' or a[1] not in (-1,1)):raise ValueError('unit move only')
+                    self.emit(op,role,a);return C(None)
+                raise ValueError('unsupported method '+op)
+            name=expr.func.id
+            if name in ('Tape','frozenset') and (expr.args or expr.keywords):raise ValueError('nonempty constructor')
+            if name=='Tape':
+                role='work'+str(len(self.roles));self.roles.append(role);return C(role)
+            if name=='frozenset':return C(frozenset())
+            args=[self.value(x,env,ns) for x in expr.args]
+            if name=='is_record':
+                z=R(self.fresh());self.emit('record',args[0],z[1]);return z
+            if name=='key_port':
+                self.inline_key(args[0],args[1]);return C(None)
+            if name=='increment':return self.call('scanner','increment_and_return',args,{})
+            if name=='evaluate_key':self.inline_key(args[0],args[1]);return C(None)
+            if name=='mark':return C(None)
+            return self.call(ns,name,args,{k.arg:self.value(k.value,env,ns) for k in expr.keywords})
+        return self.fail(expr)
+    @staticmethod
+    def compare(op,a,b):
+        if op=='eq':return a==b
+        if op=='ne':return a!=b
+        if op=='in':return a in b
+        if op=='notin':return a not in b
+        raise ValueError(op)
+    def fail(self,n):raise ValueError('unsupported AST '+ast.dump(n))
+    def assign(self,target,v,env):
+        if isinstance(target,ast.Tuple):
+            if v[0]!='tuple':
+                for i,t in enumerate(target.elts):
+                    z=R(self.fresh());self.emit('field',v,i,z[1]);self.assign(t,z,env)
+            else:
+                for t,a in zip(target.elts,v[1],strict=True):self.assign(t,a,env)
+            return
+        if not isinstance(target,ast.Name):return self.fail(target)
+        # Static aggregates contain only a fixed finite number of values/roles.
+        if v[0]=='tuple':env[target.id]=v;return
+        if target.id not in env or env[target.id][0]!='r':env[target.id]=R(self.fresh())
+        self.emit('copy',v,env[target.id][1])
+    def block(self,body,env,ns,returns,breaks,handler):
+        for n in body:
+            if isinstance(n,ast.Expr):
+                if not isinstance(n.value,ast.Constant):self.value(n.value,env,ns)
+            elif isinstance(n,ast.Assign):
+                v=self.value(n.value,env,ns)
+                for t in n.targets:self.assign(t,v,env)
+            elif isinstance(n,ast.If):
+                t=self.value(n.test,env,ns)
+                if t[0]=='c':self.block(n.body if t[1] else n.orelse,env,ns,returns,breaks,handler);continue
+                j=self.emit('branch',t,None,None);a=len(self.code);self.block(n.body,env,ns,returns,breaks,handler);end=self.emit('jump',None);b=len(self.code);self.block(n.orelse,env,ns,returns,breaks,handler);self.patch(j,'branch',t,a,b);self.patch(end,'jump',len(self.code))
+            elif isinstance(n,ast.While):
+                if n.orelse:raise ValueError('while else unsupported')
+                start=len(self.code);t=self.value(n.test,env,ns);j=self.emit('branch',t,None,None);a=len(self.code);local=[];self.block(n.body,env,ns,returns,local,handler);self.emit('jump',start);end=len(self.code);self.patch(j,'branch',t,a,end)
+                for k in local:self.patch(k,'jump',end)
+            elif isinstance(n,ast.For):
+                if n.orelse or not isinstance(n.target,ast.Name):raise ValueError('for else/target unsupported')
+                seq=self.value(n.iter,env,ns)
+                if seq[0]!='tuple':raise ValueError('only static finite for tuple')
+                for v in seq[1]:
+                    env[n.target.id]=v;self.block(n.body,env,ns,returns,breaks,handler)
+            elif isinstance(n,ast.Break):breaks.append(self.emit('jump',None))
+            elif isinstance(n,ast.Return):
+                val=C(None) if n.value is None else self.value(n.value,env,ns)
+                self.emit('copy',val,returns[0]);returns[1].append(self.emit('jump',None))
+            elif isinstance(n,ast.Raise):self.emit('halt','reject')
+            elif isinstance(n,ast.Try):
+                if n.orelse or n.finalbody:raise ValueError('try else/finally unsupported')
+                if any(not isinstance(h.type,ast.Name) or h.type.id!='ValueError' or h.name for h in n.handlers):raise ValueError('exception handler unsupported')
+                # Valid-domain theorem only; reject paths explicitly do not roll back.
+                self.block(n.body,env,ns,returns,breaks,handler)
+            else:self.fail(n)
+    def call(self,ns,name,args,kwargs):
+        if (ns,name) in self.calls:raise ValueError('recursive source not admitted')
+        fn=self.functions[ns][name];env={};params=[a.arg for a in fn.args.args]
+        if fn.decorator_list or fn.args.vararg or fn.args.kwarg or fn.args.kwonlyargs or fn.args.posonlyargs:raise ValueError('function signature unsupported')
+        if len(args)>len(params) or any(k not in params or k in params[:len(args)] for k in kwargs):raise ValueError('call arguments unsupported')
+        defaults=dict(zip(params[len(params)-len(fn.args.defaults):],fn.args.defaults))
+        for i,p in enumerate(params):
+            if i<len(args):env[p]=args[i]
+            elif p in kwargs:env[p]=kwargs[p]
+            elif p in defaults:env[p]=self.value(defaults[p],env,ns)
+            else:raise ValueError('missing static parameter '+p)
+        # Preallocate mutable locals before compiling either arm or a loop condition.
+        # Without this, the first condition could refer to an old argument register.
+        assigned={n.id for n in ast.walk(fn) if isinstance(n,ast.Name) and isinstance(n.ctx,ast.Store)}
+        for p in sorted(assigned):
+            if p in env:
+                v=env[p];env[p]=R(self.fresh());self.emit('copy',v,env[p][1])
+            else:env[p]=R(self.fresh())
+        out=self.fresh();returns=(out,[]);self.calls.append((ns,name));self.block(fn.body,env,ns,returns,[],None);self.calls.pop()
+        for j in returns[1]:self.patch(j,'jump',len(self.code))
+        return R(out)
+    def inline_key(self,counter,stream):
+        start=len(self.code);key=self.key;self.key_sites.append((start,start+len(key)))
+        mapping={'counter':counter,'stream':stream,'rom':C('rom')}
+        for role in ('h','s','offset','target','out','count','col','row','limit','u','t','y'):mapping[role]=C('key_'+role)
+        end=start+len(key)
+        for op,*a in key:
+            reg=lambda x:R('keyreg_'+x)
+            if op=='read':self.emit('read',mapping[a[0]],reg(a[1])[1])
+            elif op=='write':self.emit('write',mapping[a[0]],C(a[1]))
+            elif op=='write_reg':self.emit('write',mapping[a[0]],reg(a[1]))
+            elif op=='move':self.emit('move',mapping[a[0]],C(a[1]))
+            elif op=='set':self.emit('copy',C(a[1]),reg(a[0])[1])
+            elif op=='copy':self.emit('copy',reg(a[0]),reg(a[1])[1])
+            elif op=='eq':self.emit('eq',reg(a[0]),C(a[1]),reg(a[2])[1])
+            elif op=='eq_reg':self.emit('eq',reg(a[0]),reg(a[1]),reg(a[2])[1])
+            elif op in ('xorbit','andbit','orbit'):self.emit(op,reg(a[0]),reg(a[1]),reg(a[2])[1])
+            elif op=='branch':self.emit('branch',reg(a[0]),start+a[1],start+a[2])
+            elif op=='jump':self.emit('jump',start+a[0])
+            elif op=='halt':self.emit('jump',end) if a[0]=='accept' else self.emit('halt','reject')
+            else:raise ValueError('unlowered key opcode '+op)
diff --git a/research/crt-complete-repair-control/machine.py b/research/crt-complete-repair-control/machine.py
new file mode 100644
index 0000000000..85b7fd529f
--- /dev/null
+++ b/research/crt-complete-repair-control/machine.py
@@ -0,0 +1,137 @@
+"""Fixed finite-symbol executor and source-bound assembly entry point.
+
+Only configuration heads/PC/census are numerical observer data. Runtime
+operands are constants, finite symbol registers or fixed product fields.
+Apache-2.0; JoyboyBrian with substantial OpenAI Codex assistance.
+"""
+from pathlib import Path
+import types
+from collections import Counter
+
+def load(path):
+    m=types.ModuleType(path.stem);m.__file__=str(path)
+    exec(compile(path.read_bytes(),str(path),'exec'),m.__dict__);return m
+
+def assemble(root):
+    p=Path(__file__).parent;cmod=load(p/'compiler.py')
+    source={ns:(root/path).read_text() for ns,path in {
+        'producer':'research/crt-unary-stencil-producer/producer.py',
+        'scanner':'research/crt-dense-guard-scan/machine.py',
+        'bridge':'research/crt-mask-repair-bridge/bridge.py'}.items()}
+    query=load(root/'research/crt-uniform-rom-query/machine.py')
+    service=load(root/'research/crt-paid-key-service/service.py')
+    key,_=service.assemble(query,2)
+    c=cmod.Compiler(source,key);C=cmod.C;R=cmod.R;stages={}
+    def field(v,i):
+        reg=c.fresh();c.emit('field',v,i,reg);return R(reg)
+    stages['producer']=len(c.code)
+    produced=c.call('producer','produce',[*[C(x) for x in ('G','H','K','Y','J','B')],C('Tape')],{})
+    work=field(produced,0);stencil=field(produced,1)
+    stages['scanner']=len(c.code)
+    scanned=c.call('scanner','transduce',[stencil],{})
+    counter=field(scanned,0);mask=field(scanned,1)
+    roles=[field(work,i) for i in range(4)]
+    stages['repair']=len(c.code)
+    c.call('bridge','repair',[stencil,mask,counter,C('data'),*roles,C(None),C('increment'),C(None)],{})
+    stages['clear_control']=len(c.code)
+    for role in c.roles:c.emit('write',C(role),C('_'))
+    regs=registers(c.code)
+    for r in sorted(regs):c.emit('copy',C(None),r)
+    c.emit('halt','accept')
+    # Initialize every finite-control register through charged instructions too.
+    prefix=[('copy',C(None),r) for r in sorted(regs)]
+    prefix += [('write',C(role),C('<')) for role in c.roles]
+    shift=len(prefix)
+    lowered=[]
+    for op,*a in c.code:
+        if op=='jump':a[0]+=shift
+        elif op=='branch':a[1]+=shift;a[2]+=shift
+        lowered.append((op,*a))
+    stages={name:pc+shift for name,pc in stages.items()}
+    stages['key_sites']=[(a+shift,b+shift) for a,b in c.key_sites]
+    return tuple(prefix+lowered),tuple(c.roles),stages
+
+def registers(code):
+    found=set()
+    def walk(a):
+        if isinstance(a,tuple):
+            if len(a)==2 and a[0]=='r':found.add(a[1])
+            else:
+                for x in a:walk(x)
+    for op,*a in code:
+        for x in a:walk(x)
+        if op in ('read','copy','not','record'):found.add(a[-1])
+        elif op in ('field','eq','ne','in','notin','xorbit','andbit','orbit'):found.add(a[-1])
+    return found
+
+def execute(code,tapes,max_steps=1000000000,observe=None):
+    heads={r:0 for r in tapes};regs={r:None for r in registers(code)};pc=0;steps=0;cell=0
+    def val(a):
+        if a[0]=='c':return a[1]
+        if a[0]=='r':return regs[a[1]]
+        if a[0]=='tuple':return tuple(val(x) for x in a[1])
+        raise ValueError('invalid operand')
+    while steps<max_steps:
+        if observe is not None and pc in observe:observe[pc](pc,tapes,heads,regs,steps,cell)
+        op,*a=code[pc];steps+=1;pc+=1
+        if op=='read':
+            role=val(a[0]);regs[a[1]]=tapes[role][heads[role]];cell+=1
+        elif op=='write':
+            role=val(a[0]);tapes[role][heads[role]]=val(a[1]);cell+=1
+        elif op=='move':
+            role=val(a[0]);heads[role]+=val(a[1]);cell+=1
+            if heads[role]<0:raise ValueError('left-boundary crossing')
+            if heads[role]==len(tapes[role]):tapes[role].append('_')
+        elif op=='copy':regs[a[1]]=val(a[0])
+        elif op=='not':regs[a[1]]=not val(a[0])
+        elif op=='field':regs[a[2]]=val(a[0])[a[1]]
+        elif op=='record':
+            x=val(a[0]);regs[a[1]]=isinstance(x,tuple) and len(x)==2 and x[0]=='R' and isinstance(x[1],int) and 0<=x[1]<4096
+        elif op=='eq':regs[a[2]]=val(a[0])==val(a[1])
+        elif op=='ne':regs[a[2]]=val(a[0])!=val(a[1])
+        elif op=='in':regs[a[2]]=val(a[0]) in val(a[1])
+        elif op=='notin':regs[a[2]]=val(a[0]) not in val(a[1])
+        elif op=='xorbit':regs[a[2]]='1' if (val(a[0])=='1')!=(val(a[1])=='1') else '0'
+        elif op=='andbit':regs[a[2]]='1' if val(a[0])=='1' and val(a[1])=='1' else '0'
+        elif op=='orbit':regs[a[2]]='1' if val(a[0])=='1' or val(a[1])=='1' else '0'
+        elif op=='branch':pc=a[1] if val(a[0]) else a[2]
+        elif op=='jump':pc=a[0]
+        elif op=='halt':return dict(status=a[0],steps=steps,cell_actions=cell,heads=heads,registers=regs)
+        else:raise ValueError('unknown instruction '+op)
+    raise ValueError('observer watchdog exceeded')
+
+def control_bound(code):
+    """Longest control-only CFG path, cutting at every charged cell operation.
+
+    Explicit cycle rejection is essential. The bound then holds on every
+    executed finite path, not just the observed accepting trace.
+    """
+    edges=[]
+    for pc,(op,*a) in enumerate(code):
+        if op in ('read','write','move','halt'):out=[]
+        elif op=='jump':out=[a[0]]
+        elif op=='branch':out=[a[1],a[2]]
+        else:out=[pc+1]
+        if any(not isinstance(i,int) or not 0<=i<len(code) for i in out):raise ValueError('static CFG target')
+        edges.append(out)
+    indegree=[0]*len(code)
+    for out in edges:
+        for i in out:indegree[i]+=1
+    queue=[i for i,n in enumerate(indegree) if n==0];length=[1]*len(code);visited=0
+    while queue:
+        p=queue.pop();visited+=1
+        for q in edges[p]:
+            length[q]=max(length[q],length[p]+1);indegree[q]-=1
+            if not indegree[q]:queue.append(q)
+    if visited!=len(code):raise ValueError('unbounded control-only cycle')
+    return max(length)
+
+
+def prepare(roles,borrowed):
+    expected={'G','H','K','Y','J','B','data','rom'}
+    if set(borrowed)!=expected or len({id(v) for v in borrowed.values()})!=len(expected):
+        raise ValueError('exact distinct borrowed roles required')
+    tapes={r:['_'] for r in roles}
+    tapes.update({'key_'+r:['_'] for r in ('h','s','offset','target','out','count','col','row','limit','u','t','y')})
+    tapes.update(borrowed)
+    return tapes

From 3317e36447aaa99e51f68ccaf6c60e34edef098a Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Fri, 23 Oct 2026 02:28:00 -0700
Subject: [PATCH 2/2] Verify actual full repair caller and reject unsupported
 control forms

---
 .../crt-complete-repair-control/README.md     |  76 ++++++++++
 .../crt-complete-repair-control/RESULT.json   |  69 +++++++++
 .../crt-complete-repair-control/SOURCES.json  | 102 +++++++++++++
 .../crt-complete-repair-control/TASK.json     |  87 +++++++++++
 .../crt-complete-repair-control/VALIDATION.md |  59 ++++++++
 .../crt-complete-repair-control/VERIFY.json   |  43 ++++++
 .../crt-complete-repair-control/verify.py     | 142 ++++++++++++++++++
 7 files changed, 578 insertions(+)
 create mode 100644 research/crt-complete-repair-control/README.md
 create mode 100644 research/crt-complete-repair-control/RESULT.json
 create mode 100644 research/crt-complete-repair-control/SOURCES.json
 create mode 100644 research/crt-complete-repair-control/TASK.json
 create mode 100644 research/crt-complete-repair-control/VALIDATION.md
 create mode 100644 research/crt-complete-repair-control/VERIFY.json
 create mode 100644 research/crt-complete-repair-control/verify.py

diff --git a/research/crt-complete-repair-control/README.md b/research/crt-complete-repair-control/README.md
new file mode 100644
index 0000000000..9a7317fa41
--- /dev/null
+++ b/research/crt-complete-repair-control/README.md
@@ -0,0 +1,76 @@
+# Complete finite control at the actual CRT repair caller
+
+The #4795 key service prices its instructions, but its real surrounding
+producer/scanner/repair caller still executes Boolean control in Python and
+prices only cell actions. This package lowers the unchanged source ASTs to
+one fixed finite-symbol program and executes the complete actual layer:
+unary geometry, stencil, dense mask, split, 2,944 direct key calls, stable
+12-pass radix repair, reinsertion and disposal. Runtime execution has no
+Python source loop, callable key, AST interpretation or host-generated mask.
+
+The successful-domain theorem covers the fixed u2/t2/y8 geometry, arbitrary
+opaque 12-bit record labels, and any target-independent 32-bit ROM at target
+position 2. The actual canonical fixture has 4,096 records and the source
+h3/modulus5/offsets[0,2,4,0] middle layer. Raw post-S data and the supplied
+ROM remain explicit inputs. No raw compact macro, twelve-shuttle native
+implementation, all-size E(p,ell), binary transition table or new kappa is
+claimed.
+
+`compiler.py` expands finite source calls and relocates the entire retained
+key program into the split continuation. Mutable locals, short-circuit
+conditions, marker loops, fixed role multiplexers and finite stencil/record
+symbols all have explicit instruction semantics. Unsupported syntax is
+rejected, including loop-else and try-finally. On malformed-input errors the
+compiler rejects without claiming the original producer's exception cleanup.
+`machine.py` installs and disposes of owned markers and initializes/resets
+all finite-control registers through charged instructions.
+
+The full static CFG is cut at charged tape operations; its remaining graph
+must be acyclic. Its longest path D bounds every control-only interval, so
+T <= (D+1)(C+1), for any execution with C cell actions. The written proof
+also bounds all outer actions and every retained key call, without re-adding
+the removed host key interface. This completes one local instruction ledger;
+it does not claim an improved asymptotic tariff.
+
+## Reproduce
+
+```
+python3.12 -B scripts/research_package.py --package research/crt-complete-repair-control
+```
+
+`verify.py --light` runs bounded CFG, compiler admission, nested key, radix,
+carry, cleanup and alias controls. Full verification checks every actual key
+against an independent source oracle, the entire repaired payload, exact bad-only
+call set, all borrowed/private roles and heads, and the frozen instruction
+receipt. `--write-result` is explicit authoring mode. Exact source/history,
+normal/optimized, export and corruption evidence is recorded in VALIDATION.md.
+
+The constructor only allocates fixed blank owned roles and verifies borrowed
+object disjointness; it never decodes the unary headers, ROM or payload into
+execution decisions. Verifier callbacks observe execution and cannot supply
+an operand, key or branch. The local theorem assumes correctly framed inputs;
+there is no blanket malformed-input rollback claim.
+
+## Open next questions
+
+1. Lower the whole finite alphabet to binary transitions, with its full constant.
+2. Execute raw compact S and its twelve paid dirty-back shuttles on the same data.
+3. Connect variable-geometry descriptor/ROM/key generation and the full E bill.
+
+TASK.json records concrete first steps and blockers. These obligations remain
+separate from the completed fixed caller and are not automatic continuation.
+
+## Provenance and credit
+
+Base81e9bd69e4a5b00ba9c713a1620e36d576d5522e, priority7. Canonical claim:
+https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19142272
+
+Credit Cinna Davis #4100 for the compact CRT construction and source oracle;
+Hiroki KUMAZAKI #4169/#4174 for current-state reverse keys; ToikY #4201/#4208
+for scanner/producer; the #4637 mask bridge, Jose Manuel and Ryanson Jonathan
+for retained repair lineage; unpaidmoon and Douglas Colkitt/OpenAI; and the
+#4795/#4752 finite-key/query predecessors. Their source algorithms and proofs
+are reused, not presented as new. All source files and original notices remain
+unchanged and hash-pinned. JoyboyBrian, with substantial OpenAI Codex assistance.
+Apache-2.0. Separate agent review is not independent human or proof-kernel
+acceptance. Selected frontier and frozen archives are unchanged.
diff --git a/research/crt-complete-repair-control/RESULT.json b/research/crt-complete-repair-control/RESULT.json
new file mode 100644
index 0000000000..dd1978ed60
--- /dev/null
+++ b/research/crt-complete-repair-control/RESULT.json
@@ -0,0 +1,69 @@
+{
+  "status": "PASS_COMPLETE_CRT_REPAIR_CONTROL",
+  "source_hashes": {
+    "research/crt-unary-stencil-producer/producer.py": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0",
+    "research/crt-unary-stencil-producer/PROOF.md": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa",
+    "research/crt-dense-guard-scan/machine.py": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7",
+    "research/crt-dense-guard-scan/PROOF.md": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11",
+    "research/crt-mask-repair-bridge/bridge.py": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331",
+    "research/crt-mask-repair-bridge/key_subroutine.py": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44",
+    "research/crt-mask-repair-bridge/PROOF.md": "c74f93a65f7b28e751a9c93aa37fc7f74f7ce42cd96e31fa3d1212c94991769c",
+    "research/crt-paid-key-service/service.py": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083",
+    "research/crt-paid-key-service/PROOF.md": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325",
+    "research/crt-uniform-rom-query/machine.py": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d",
+    "research/crt-uniform-rom-query/PROOF.md": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870",
+    "research/unconditional-batched-crt/check_batched_crt.py": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e",
+    "research/unconditional-batched-crt/CRT.md": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b",
+    "research/unconditional-batched-crt/NOTICE.md": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461"
+  },
+  "controls": {
+    "rejected": [
+      "try_finally",
+      "while_else",
+      "for_else",
+      "nonempty_tape",
+      "method_extra_arg",
+      "keep_buckets",
+      "skip_pass",
+      "carry_skipped_bit",
+      "control_only_cycle",
+      "borrowed_role_alias",
+      "skipped_nested_key",
+      "borrowed_rom_write"
+    ],
+    "control_factor": 606,
+    "program_instructions": 8242
+  },
+  "actual": {
+    "status": "PASS_ACTUAL_COMPLETE",
+    "program": 8242,
+    "steps": 167388895,
+    "cells": 52900280,
+    "factor": 606,
+    "key_calls": 2944,
+    "phases": {
+      "616": [
+        616,
+        11
+      ],
+      "1532": [
+        2862,
+        852
+      ],
+      "1758": [
+        2637861,
+        455682
+      ],
+      "7625": [
+        167388278,
+        52900269
+      ]
+    },
+    "program_sha256": "ed1893ec1eb99f075fb67b5319cf99e961d3f9bb0daba82c13a84cbe4dfb28bf"
+  },
+  "code_hashes": {
+    "compiler.py": "1186cdefed22890a987c1f289290c6db4c19446a29461c1db46257f318b05156",
+    "machine.py": "afa110ed2fdba62e810fd794e5fd62a07ec4caf18e8919066275523713353cc7"
+  },
+  "instruction_bound": 6294271835487
+}
diff --git a/research/crt-complete-repair-control/SOURCES.json b/research/crt-complete-repair-control/SOURCES.json
new file mode 100644
index 0000000000..513b47f593
--- /dev/null
+++ b/research/crt-complete-repair-control/SOURCES.json
@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "research/crt-unary-stencil-producer/producer.py",
+      "usage": "input",
+      "git_blob": "dd357a0679c244e5d95b2b782bd70ea9f2507795",
+      "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0"
+    },
+    {
+      "path": "research/crt-unary-stencil-producer/PROOF.md",
+      "usage": "input",
+      "git_blob": "d81a6cca7c433bc7fb015a41cc0f72bf9f676a5d",
+      "sha256": "4076e6041bedce5269c1d4e3d62f0e4213a4b2e790fe270b89b4b4f3363e08aa"
+    },
+    {
+      "path": "research/crt-dense-guard-scan/machine.py",
+      "usage": "input",
+      "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82",
+      "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7"
+    },
+    {
+      "path": "research/crt-dense-guard-scan/PROOF.md",
+      "usage": "input",
+      "git_blob": "235d7405ffcf712ad3905c3077719554ade0790c",
+      "sha256": "c075a3c261bb824884f0da9f99fed227b15f9fac087bbdeb2c2cb861d4091f11"
+    },
+    {
+      "path": "research/crt-mask-repair-bridge/bridge.py",
+      "usage": "input",
+      "git_blob": "826d62adbb777ceec20974e600a6ea05e03b7828",
+      "sha256": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331"
+    },
+    {
+      "path": "research/crt-mask-repair-bridge/key_subroutine.py",
+      "usage": "input",
+      "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c",
+      "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44"
+    },
+    {
+      "path": "research/crt-mask-repair-bridge/PROOF.md",
+      "usage": "input",
+      "git_blob": "e6138f3b6c0920f84422a1022064e14e2daea76b",
+      "sha256": "c74f93a65f7b28e751a9c93aa37fc7f74f7ce42cd96e31fa3d1212c94991769c"
+    },
+    {
+      "path": "research/crt-paid-key-service/service.py",
+      "usage": "input",
+      "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517",
+      "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083"
+    },
+    {
+      "path": "research/crt-paid-key-service/PROOF.md",
+      "usage": "input",
+      "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9",
+      "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325"
+    },
+    {
+      "path": "research/crt-uniform-rom-query/machine.py",
+      "usage": "input",
+      "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077",
+      "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d"
+    },
+    {
+      "path": "research/crt-uniform-rom-query/PROOF.md",
+      "usage": "input",
+      "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f",
+      "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870"
+    },
+    {
+      "path": "research/unconditional-batched-crt/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "input",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "research/unconditional-batched-crt/NOTICE.md",
+      "usage": "input",
+      "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f",
+      "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461"
+    }
+  ]
+}
diff --git a/research/crt-complete-repair-control/TASK.json b/research/crt-complete-repair-control/TASK.json
new file mode 100644
index 0000000000..8439e00a9b
--- /dev/null
+++ b/research/crt-complete-repair-control/TASK.json
@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Execute and price complete outer finite control at the actual fixed CRT producer/scanner/key/radix/reinsert caller.",
+  "scope_change_reason": "PR4795 Open next question2 leaves outer Boolean/control costs after the actual key instructions were closed.",
+  "bottleneck_link": "Closes a complete actual caller instruction and ownership boundary; raw compact macro and full evaluator remain external.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at this fixed real caller or a precise missing control/ownership contract.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, RESULT.json, verify.py and VALIDATION.md; actual4096-record/2944-key caller.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance and separate agent review; no independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Lower the complete caller alphabet to actual binary transitions.",
+      "why_it_matters": "Finite-symbol operation counts do not establish a binary constant for opaque record and stencil symbols.",
+      "first_step": "Apply a source-pinned fixed code to the entire static program and execute one positive-ROM nested return.",
+      "blocked_by": "Not part of this finite-symbol proof."
+    },
+    {
+      "question": "Execute raw compact S with the twelve dirty-back shuttles before this repair.",
+      "why_it_matters": "The repaired caller starts at a supplied post-S data stream.",
+      "first_step": "Bind the first t-update shuttle to the actual ordinary physical port with all dirty back-field values.",
+      "blocked_by": "Native record representation and complete-fiber rotation lifecycle remain external."
+    },
+    {
+      "question": "Compose variable-geometry descriptor, ROM and key production with the full evaluator bill.",
+      "why_it_matters": "This closes actual fixed outer control, not all-size E(p,ell).",
+      "first_step": "Bind one encoded larger header to the current-state query and retain owned descriptor/ROM disposal.",
+      "blocked_by": "The retained key service has fixed u2/t2/y8 geometry."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19142272"
+}
diff --git a/research/crt-complete-repair-control/VALIDATION.md b/research/crt-complete-repair-control/VALIDATION.md
new file mode 100644
index 0000000000..b8ddb30e41
--- /dev/null
+++ b/research/crt-complete-repair-control/VALIDATION.md
@@ -0,0 +1,59 @@
+# Validation
+
+Environment: macOS, CPython3.12.2, standard library only. Scientific replays
+were serialized through the batch's sole heavy slot. No Lean, Docker,
+selected-frontier or historical full suite was run.
+
+The first complete actual source fixture passed with 4,096 opaque payloads,
+2,944 independently checked current-state keys, 167,388,873 instructions and
+52,900,258 cell actions in35.78 seconds. This was a calibration before the
+explicit22 owned-marker lifecycle writes. The final program adds those writes,
+makes static register allocation deterministic and rejects unsupported AST
+forms. No earlier receipt is relabelled as final evidence.
+
+The bounded final controls pass: try-finally, while-else, for-else, nonempty
+Tape construction, extra method argument, bucket-clear omission, skipped radix
+pass, skipped carry bit, control-only cycle, borrowed-role alias, skipped
+nested key and changed borrowed-ROM bytes. An isolated corrupted retained
+producer source is rejected by SHA256 authentication before assembly/replay.
+The actual nested-key probe uses a positive ROM, preserves the opaque prefix
+and erases key scratch.
+
+Independent read-only agent review covered static AST semantics/admission,
+finite-role/finite-symbol boundaries, direct relocated key return, CFG bound,
+source proof and ownership. Two findings were fixed: unsupported source
+finally/loop-else/argument forms now reject, and the actual full verifier now
+snapshots and checks the exact six borrowed unary tapes and ROM, including
+framing and tails. Final reviewed SHA256:
+
+* compiler.py:1186cdefed22890a987c1f289290c6db4c19446a29461c1db46257f318b05156
+* machine.py:afa110ed2fdba62e810fd794e5fd62a07ec4caf18e8919066275523713353cc7
+* PROOF.md:151211f34d80c8edd03512dd18af27b9b5b1dfe6f9fda9f904bfd59c4ab1a807
+* verify.py:167e3d45c2edfa74eccffaf8929ebdd95b3c5b0623339b1ab1329bff0e156589
+
+This is agent review, not independent human or formal-kernel acceptance.
+
+Final full normal authoring replay uses
+`python3.12 -B research/crt-complete-repair-control/verify.py --write-result`.
+This executes every registered check; only the final receipt write replaces
+receipt equality. Final normal/optimized/export outcomes are recorded below. The static program hash is
+ed1893ec1eb99f075fb67b5319cf99e961d3f9bb0daba82c13a84cbe4dfb28bf;
+8,242 instructions and longest control-only path606. The conservative total
+instruction upper bound is6,294,271,835,487; it is not an observed runtime
+or a complete E(p,ell) bound.
+
+Final normal replay PASS:167,388,895 instructions,52,900,280 cell actions,
+2,944 exact marked-key calls; all twelve controls, borrowed bytes, data,
+heads, private storage and control reset pass. The22-action delta from the
+first calibration is exactly the newly executed marker lifecycle. Metadata
+and exact source pins pass. Committed-byte/source-history check and official export/check passed at
+dcebc47566b92dabce1c57fb7beb6cff3eb6adf7 (24 package/input files).
+
+The official archive SHA256 was
+11bfc17135bf0bfc3258d896211d96deb1be438582740606f9c503f39e6876a8.
+Extracted without .git metadata, with PATH set to an empty directory,
+`/opt/local/bin/python3.12 -O -B research/crt-complete-repair-control/verify.py`
+passed the complete frozen receipt:167,388,895 instructions,52,900,280 cells,
+2,944 key calls and all twelve controls. Every exported file remained byte
+identical after replay. Subsequent changes only record this validation; all
+scientific executables, proof, inputs and receipt bytes remain unchanged.
diff --git a/research/crt-complete-repair-control/VERIFY.json b/research/crt-complete-repair-control/VERIFY.json
new file mode 100644
index 0000000000..a158cc4198
--- /dev/null
+++ b/research/crt-complete-repair-control/VERIFY.json
@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/crt-unary-stencil-producer/producer.py",
+    "research/crt-unary-stencil-producer/PROOF.md",
+    "research/crt-dense-guard-scan/machine.py",
+    "research/crt-dense-guard-scan/PROOF.md",
+    "research/crt-mask-repair-bridge/bridge.py",
+    "research/crt-mask-repair-bridge/key_subroutine.py",
+    "research/crt-mask-repair-bridge/PROOF.md",
+    "research/crt-paid-key-service/service.py",
+    "research/crt-paid-key-service/PROOF.md",
+    "research/crt-uniform-rom-query/machine.py",
+    "research/crt-uniform-rom-query/PROOF.md",
+    "research/unconditional-batched-crt/check_batched_crt.py",
+    "research/unconditional-batched-crt/CRT.md",
+    "research/unconditional-batched-crt/NOTICE.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exact source authentication, actual complete4096-record/2944-key controller, full instruction/control bound, ownership, deterministic program and semantic/AST controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Same full source-bound checks and frozen receipt with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/crt-complete-repair-control/verify.py b/research/crt-complete-repair-control/verify.py
new file mode 100644
index 0000000000..f5e21ae8ef
--- /dev/null
+++ b/research/crt-complete-repair-control/verify.py
@@ -0,0 +1,142 @@
+from pathlib import Path
+import types,time,json,hashlib,argparse
+p=Path(__file__).resolve().parent;r=p.parents[1]
+def load(f):
+ m=types.ModuleType(f.stem);m.__file__=str(f);exec(compile(f.read_bytes(),str(f),'exec'),m.__dict__);return m
+
+def actual():
+ m=load(p/'machine.py');crt=load(r/'research/unconditional-batched-crt/check_batched_crt.py');oracle=load(r/'research/crt-mask-repair-bridge/key_subroutine.py')
+ rows=[crt.benes(crt.rotation(8,5,a))[2][1] for a in (0,2,4,0)];bits=tuple(b for row in rows for b in row);key=oracle.ReverseWordKey(2,bits)
+ raw=[None]*4096;ideal=[None]*4096;holes=set()
+ for x in range(4096):
+  u,t,y=x>>10,(x>>8)&3,x&255
+  v=crt.compact(u,t,y,lambda z:(bits[z&31],),positions=(2,),ybits=8)
+  dest=(v[0]<<10)|(v[1]<<8)|v[2];raw[dest]=('R',x)
+  ideal[(u<<10)|(t<<8)|(y^(bits[y&31]<<2))]=('R',x)
+  if not crt.good(u,t,y,bits=2,positions=(2,),guard=6):holes.add(x)
+ code,roles,stages=m.assemble(r);tapes={};tapes.update({x:['<',*('1'*v),'>','_'] for x,v in zip(('G','H','K','Y','J','B'),(2,2,6,8,2,0))});tapes['data']=['<',*raw,'>'];tapes['rom']=['L',*map(str,bits),'R'];tapes=m.prepare(roles,tapes)
+ borrowed_before={x:list(tapes[x]) for x in ('G','H','K','Y','J','B','rom')}
+ seen=[];phases={};key_start,key_end=stages['key_sites'][0];active={}
+ def entry(pc,t,h,reg,steps,cells):
+  q=int(''.join(t['work9'][1:13]),2);seen.append(q);active.update(q=q,start=h['work1'],steps=steps,cells=cells)
+ def returned(pc,t,h,reg,steps,cells):
+  want=key.key_of(f"{active['q']:012b}");got=''.join(t['work1'][active['start']:h['work1']]);
+  if got!=want:raise ValueError(('actualkey',active['q'],got,want))
+  if any(any(c!='_' for c in t[x]) or h[x] for x in t if x.startswith('key_')):raise ValueError('keycleanup')
+ def phase(pc,t,h,reg,steps,cells):phases[pc]=(steps,cells)
+ obs={key_start:entry,key_end:returned};obs.update({v:phase for k,v in stages.items() if k!='key_sites'})
+ t=time.monotonic();out=m.execute(code,tapes,observe=obs);seconds=time.monotonic()-t
+ if out['status']!='accept' or tapes['data']!=['<',*ideal,'>']:raise ValueError('fullendpoint')
+ check_borrowed(borrowed_before,tapes)
+ if seen!=sorted(holes):raise ValueError('actualholecalls')
+ if any(out['heads'].values()):raise ValueError('heads')
+ if any(any(v!='_' for v in tapes[x]) for x in roles):raise ValueError('privateblank')
+ if any(v is not None for v in out['registers'].values()):raise ValueError('controlerase')
+ return dict(status='PASS_ACTUAL_COMPLETE',program=len(code),steps=out['steps'],cells=out['cell_actions'],factor=m.control_bound(code),key_calls=len(seen),phases={str(k):list(v) for k,v in phases.items()},program_sha256=hashlib.sha256(json.dumps(code,separators=(',',':')).encode()).hexdigest())
+
+def check_borrowed(before,tapes):
+ for name,cells in before.items():
+  if tapes[name]!=cells:raise ValueError('borrowed bytes changed '+name)
+
+def need(ok,label):
+ if not ok:raise ValueError(label)
+
+def authenticate():
+ hashes={}
+ for row in json.loads((p/'SOURCES.json').read_text())['files']:
+  if row['usage']!='input':continue
+  raw=(r/row['path']).read_bytes();h=hashlib.sha256(raw).hexdigest()
+  need(h==row['sha256'],'source hash '+row['path'])
+  need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==row['git_blob'],'source blob')
+  hashes[row['path']]=h
+ return hashes
+
+def controls():
+ m=load(p/'machine.py');cm=load(p/'compiler.py');C=cm.C
+ src={ns:(r/path).read_text() for ns,path in {'bridge':'research/crt-mask-repair-bridge/bridge.py','scanner':'research/crt-dense-guard-scan/machine.py'}.items()}
+ def radix(fault=None):
+  c=cm.Compiler(src,[]);flags=C(frozenset({'keep_buckets'}) if fault=='keep_buckets' else frozenset())
+  c.call('bridge','sort_passes',[C('stencil'),C('bad'),C('b0'),C('b1'),flags],{});c.emit('halt','accept')
+  keys=[6,1,7,0,5,2,4,3];cells=['<']
+  for label,key in enumerate(keys):cells.extend([('R',label),*f'{key:03b}'])
+  cells.append('>');tapes=dict(stencil=['<','1','1','1','>'],bad=cells,b0=['<'],b1=['<'])
+  code=list(c.code)
+  if fault=='skip_pass':tapes['stencil']=['<','1','1','>']
+  result=m.execute(code,tapes,max_steps=100000)
+  expected=['<']
+  for label,key in sorted(enumerate(keys),key=lambda z:z[1]):expected.extend([('R',label),*f'{key:03b}'])
+  expected.append('>')
+  need(tapes['bad']==expected,'full key sort and key rotation')
+  need(all(all(x=='_' for x in tapes[t][1:]) for t in ('b0','b1')),'bucket cleanup')
+  need(not any(result['heads'].values()),'radix head return')
+ radix();rejected=[]
+ for label,text in [
+  ('try_finally','def f(t):\n try:\n  t.read()\n finally:\n  t.write(1)\n'),
+  ('while_else','def f(t):\n while False:\n  t.read()\n else:\n  t.write(1)\n'),
+  ('for_else','def f(t):\n for x in (1,):\n  t.read()\n else:\n  t.write(1)\n'),
+  ('nonempty_tape','def f(t):\n a = Tape(1)\n'),
+  ('method_extra_arg','def f(t):\n t.read(1)\n')]:
+  c=cm.Compiler({'probe':text},[])
+  try:c.call('probe','f',[C('t')],{})
+  except ValueError:rejected.append(label)
+  else:raise ValueError('unsupported AST accepted '+label)
+
+ for fault in ('keep_buckets','skip_pass'):
+  try:radix(fault)
+  except ValueError:rejected.append(fault)
+  else:raise ValueError('missed '+fault)
+ def carry(skip):
+  c=cm.Compiler(src,[])
+  for _ in range(5):c.emit('move',C('counter'),C(1))
+  ret=c.call('scanner','increment_and_return',[C('counter'),C(skip)],{});c.emit('halt','accept')
+  tapes={'counter':['<','1','1','1','1','>']};out=m.execute(c.code,tapes)
+  need(tapes['counter']==['<','0','0','0','0','>'] and out['heads']['counter']==0 and out['registers'][ret[1]] is False,'complete carry wrap')
+ carry(False)
+ try:carry(True)
+ except ValueError:rejected.append('carry_skipped_bit')
+ else:raise ValueError('missed carry fault')
+ code,roles,stages=m.assemble(r);factor=m.control_bound(code)
+ bad=list(code);bad[0]=('jump',0)
+ try:m.control_bound(bad)
+ except ValueError:rejected.append('control_only_cycle')
+ else:raise ValueError('cycle accepted')
+ shared=['<','>'];borrowed={x:list(shared) for x in ('G','H','K','Y','J','B','data','rom')};borrowed['H']=borrowed['G']
+ try:m.prepare(roles,borrowed)
+ except ValueError:rejected.append('borrowed_role_alias')
+ else:raise ValueError('alias accepted')
+ # Actual producer/scanner/split path and positive-ROM key return, bounded at first call.
+ def nested(skip_key=False):
+  tapes={x:['<',*('1'*v),'>','_'] for x,v in zip(('G','H','K','Y','J','B'),(2,2,6,8,2,0))};tapes.update(data=['<',('R',123),'>'],rom=['L',*('1'*32),'R']);tapes=m.prepare(roles,tapes)
+  short=list(code);entry,end=stages['key_sites'][0];short[end]=('halt','accept')
+  if skip_key:short[entry]=('jump',end)
+  out=m.execute(short,tapes,max_steps=4000000)
+  key=load(r/'research/crt-mask-repair-bridge/key_subroutine.py').ReverseWordKey(2,(1,)*32).key_of('0'*12)
+  need(tapes['work1'][1:14]==[('R',123),*key] and out['heads']['work1']==14,'direct nested key return and opaque prefix')
+  need(all(all(v=='_' for v in tapes[x]) and out['heads'][x]==0 for x in tapes if x.startswith('key_')),'key private cleanup')
+ nested()
+ try:nested(True)
+ except ValueError:rejected.append('skipped_nested_key')
+ else:raise ValueError('skipped key accepted')
+ before={'rom':['L','0','R']};changed={'rom':['L','1','R']}
+ try:check_borrowed(before,changed)
+ except ValueError:rejected.append('borrowed_rom_write')
+ else:raise ValueError('borrowed corruption accepted')
+ # Every emitted opcode has a finite instruction interpretation, never a source callback.
+ allowed={'read','write','move','copy','not','field','record','eq','ne','in','notin','xorbit','andbit','orbit','branch','jump','halt'}
+ need(all(i[0] in allowed for i in code),'instruction allowlist')
+ need(code==m.assemble(r)[0],'deterministic static program')
+ return dict(rejected=rejected,control_factor=factor,program_instructions=len(code))
+
+def main():
+ ap=argparse.ArgumentParser();ap.add_argument('--light',action='store_true');ap.add_argument('--write-result',action='store_true');args=ap.parse_args()
+ sources=authenticate();checks=controls()
+ if args.light:print('PASS_REPAIR_CONTROL_LIGHT',json.dumps(checks));return
+ result={'status':'PASS_COMPLETE_CRT_REPAIR_CONTROL','source_hashes':sources,'controls':checks,'actual':actual(),
+         'code_hashes':{f:hashlib.sha256((p/f).read_bytes()).hexdigest() for f in ('compiler.py','machine.py')}}
+ a=result['actual'];bound=(a['factor']+1)*(1000*4096*13**2+2944*3287110+1)
+ need(a['steps']<=bound,'complete conservative instruction bound');result['instruction_bound']=bound
+ if args.write_result:(p/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n')
+ else:need(json.loads((p/'RESULT.json').read_text())==result,'frozen full receipt')
+ print(result['status'],a['steps'],a['cells'],a['key_calls'])
+
+if __name__=='__main__':main()