R12 Operator-Balanced Commit Bisimulation preregistration

Status: CPU structural falsifier only. No neural fit, H100 job, or Shohin checkpoint modification is authorized before the already-running carry-only writer experiment has a sealed score. A CPU pass establishes internal consistency and rejects named shortcuts; it is not evidence that Shohin learned the mechanism.

1. Question and empirical boundary

Shohin's post-DRS evidence is consistent with a narrow transaction failure:

• the frozen model often computes the active digit correctly;
• a late residual linearly exposes carry;
• forcing carry and digit tokens repairs the serialized state;
• the next call responds to a carry intervention in most, but not all, cases;
• autonomous repeated execution still fails.

The live carry-only motor tests the smallest immediate hypothesis: repair only the carry writer and leave the frozen reader untouched. OBCB-1 is a conditional successor, not a competing launch. It asks whether a source-independent one-bit commit protocol is easier to learn when supervision is allocated by the algebraic carry operator rather than by marginal output labels.

The allowed claim is deliberately narrow:

Equal allocation over the three decimal carry transformations, paired counterfactual supervision, and a hard one-bit source-deletion boundary may improve learnability and closed-loop composition at matched data and compute.

OBCB-1 is not a new computational primitive, a new model class, or evidence of general reasoning.

2. Exact finite machine

For operation op, decimal digits a,b, and incoming carry or borrow c in {0,1}, define

[ T_{op,a,b}(c)=(d,c'). ]

For addition,

[ s=a+b+c,\quad d=s\bmod 10,\quad c'=\mathbf{1}[s\ge 10]. ]

For subtraction,

[ s=a-b-c,\quad d=s\bmod 10,\quad c'=\mathbf{1}[s<0]. ]

For fixed (op,a,b), the carry update is exactly one of

[ K_0(c)=0,\qquad I(c)=c,\qquad K_1(c)=1. ]

The partition is:

Each operation has exactly 45 K0, 10 I, and 45 K1 digit pairs. Under composition, {K0,I,K1} is a three-element transformation monoid. I is the identity; composing a constant map after any map returns that constant map.

The two carry states are minimal. For example, addition with (a,b)=(0,0) emits different digits for c=0 and c=1. One bit is therefore necessary and sufficient when operation, operands, and cursor remain visible.

3. OBCB-1 allocation and boundary

The 200 (op,a,b) events are partitioned by monoid element before sampling. Counterfactual rows for c=0 and c=1 are inseparable pairs. The smallest uniform integer allocation over every underlying digit pair uses the least common multiple of 45 and 10:

• each K0 pair is repeated twice;
• each I pair is repeated nine times;
• each K1 pair is repeated twice.

This produces, per operation, 90 paired examples and 180 rows for each monoid element. Across addition and subtraction the frozen allocation has 540 paired examples and 1,080 rows. No pair may be split between arms or batches used for the matched comparison.

After one transition, only

CommitBit(bit: bool)

may cross the boundary. The prior event, source digits, incoming bit, emitted digit, generated history, KV state, cursor history, and step number are deleted. The next transition receives only the next visible event and CommitBit. Gradients stop at this discrete semantic boundary in any future neural realization.

The protocol adds zero trainable parameters. A future learned realization may use an ordinary adapter only if every learned arm receives the same adapter, initialization, update budget, and optimizer. OBCB does not claim the adapter.

4. Counterfactual bisimulation law

Let J(c)=1-c. For each local event x=(op,a,b), the two factual outputs must obey:

[ T_x(Jc)=\Psi_x(T_x(c)), ]

where Psi_x swaps exactly the two valid outputs. More concretely:

• addition changes the digit by +1 mod 10 under a carry flip;
• subtraction changes the digit by -1 mod 10;
• K0 leaves outgoing carry zero;
• K1 leaves outgoing carry one;
• I flips outgoing carry with the input.

The carry signatures are

[ K_0J=K_0,\qquad K_1J=K_1,\qquad IJ=JI=J. ]

If all 400 local cells are exact, every output packet satisfies the one-bit contract, and every one of the 40,000 same-operation two-step edges is closed, then exact iteration follows by induction for any finite sequence. The CPU falsifier checks the induction base and every length-two composable edge; it does not infer neural learnability from that fact.

5. Frozen CPU falsifier

pipeline/obcb_falsifier.py must deterministically:

1. enumerate all 200 local events and classify them as K0, I, or K1;
2. verify the 45/10/45 counts separately for addition and subtraction;
3. verify monoid closure, identity, and all 27 associativity triples;
4. enumerate all 400 (op,a,b,c) cells and compare against an independent decimal oracle;
5. verify all 200 paired carry-flip signatures;
6. construct and hash the 1,080-row operator-balanced paired allocation;
7. enumerate all 40,000 tuples (operation, first_pair, second_pair, initial_carry);
8. verify factual and flipped two-step execution, exact packet closure, source poisoning invariance, and absence of machine-internal retained state;
9. inspect packet structure rather than trusting a self-reported resource ledger; and
10. reject every named negative control.

The CPU decimal oracle is explicitly an external verifier used by the falsifier. It is forbidden at neural inference and cannot support a learned reasoning claim.

6. Required negative controls

The finite board must reject:

1. Commit-ignoring: computes every transition as if incoming carry were zero.
2. Stale-source replay: is behaviorally exact while its retained source is intact, but recomputes the committed bit from the prior event. It must fail structural source deletion and change under source poisoning.
3. Shuffled state: deterministically swaps carry labels for a balanced subset of event pairs while retaining the one-bit packet shape.
4. Result history: carries the correct bit plus the prior result digit. It may be behaviorally exact but must fail the one-bit packet contract.
5. Hidden step: carries the correct bit plus a hidden transition counter. It may be behaviorally exact but must fail the one-bit packet contract.

A favorable cheating control is allowed to remain behaviorally exact. It is still rejected if it retains forbidden information. Conversely, a resource-matched one-bit control is rejected only by a frozen behavioral gate.

7. Equivalence dossier and allowed novelty

OBCB-1 has no favorable expressivity separation from established methods:

• Ordinary counterfactual paired SFT: same zero-loss function class. OBCB differs only in operator allocation and the enforced deletion boundary.
• One-bit recurrence / two-state automaton: exactly isomorphic to the minimal carry transducer and the strongest favorable architectural control.
• RNN, GRU, or tied transformer recurrence: can realize the same state update; at fixed width it can be unrolled into a finite circuit.
• Adapter or LoRA implementation: ordinary implementation machinery. If needed, the same parameter budget must be granted to every learned arm.
• A 400-cell table: exactly realizes the local transition and is a required upper-bound control, not a learned systematicity claim.
• Visible state tokens or KV memory: can realize the bit but must charge token and KV resources. They are favorable controls with a larger retained information vector.
• External executor or result tape: can solve the task but violates the source-deletion and no-external-execution contract.

The only reopenable conjecture is a learnability and sample-allocation claim: balancing by transition-monoid element and enforcing one-bit causal closure may outperform outcome-balanced paired SFT at equal examples, parameters, updates, and inference steps.

8. Frozen resource vector

For the OBCB mechanism relative to its matched learner:

Training examples, optimizer updates, FLOPs, precision, adapter parameters, and base checkpoint must be identical in every future neural arm. The CPU falsifier's oracle calls are reported as verification work, not inference.

9. Neural matched arms, conditional only

No arm below may launch until the carry-only writer result is sealed and interpreted.

1. existing frozen reader plus successful writer only;
2. ordinary outcome-balanced counterfactual paired SFT;
3. operator-balanced paired SFT without deletion enforcement;
4. OBCB-1 with operator balance and hard one-bit deletion;
5. favorable explicit one-bit recurrent register;
6. equal-budget generic rank-8 adapter;
7. shuffled state within identical nuisance strata;
8. 400-cell table upper bound.

All arms share data identities, total examples, optimizer updates, batch order, base, adapter capacity, and decode policy. Development can reject but cannot confirm. A one-shot held-out board must be frozen before any score is read.

10. Kill criteria

Reject the finite OBCB contract if any of these occur:

• a local cell or carry-flip signature fails;
• an operation does not have exact 45/10/45 monoid counts;
• one of 40,000 composable edges fails factual, flipped, or source-poisoned execution;
• any packet retains more than the exact boolean bit;
• any machine object retains source, result history, or step state;
• a named negative control is admitted;
• the deterministic report changes across repeated runs.

If a later neural experiment is authorized, reject the OBCB hypothesis if:

• fresh writer accuracy is below 99%;
• identity-class carry accuracy or flip selectivity is below 99.5%;
• any operation, style, width, or carry stratum is below 99%;
• source poisoning or irrelevant sham interventions alter continuation;
• the frozen cycle remains below 45/50;
• full traces remain below 90% separately at widths 4, 6, 8, and 10;
• OBCB gains less than 10 points over operator-balanced paired SFT on cycles or less than 15 points on unseen-width full traces;
• shuffled labels retain more than 25% of treatment gain; or
• local gates pass while closed cycles fail. That outcome falsifies one-bit sufficiency for the deployed interface and forbids silently adding a tape.

If ordinary paired SFT, the one-bit recurrent control, or the matched adapter ties OBCB, retain the simpler method and reject any OBCB-specific advantage.