Cassette Build Report 046 — Independent Arithmetic Was Not Independent Enough
S19's publication guard used two code paths for one calculation, so a shared mathematical mistake could have passed until independent arithmetic and syntax checks were added.
Scope note: This report covers S19’s certificate publication gate and its arithmetic repair. It distinguishes containment evidence from mathematical independence; it does not claim that the compiler is a general model compiler or that every theorem behind Cassette has been independently proved.
S19 had the right publication shape. The compiler derived a certificate from canonical bytes. The broker and pager checked that certificate before generation publication. The compiler’s own structural verifier did not pretend to be the final mathematical authority.
One word carried too much of the guarantee: independent.
Opus 5 Max compared the arithmetic in compiler.py and pager.py. The files were separate, as the repository’s sibling rule required. The multiplication, rank, determinant, and inner-product helpers were still the same algorithms, copied into two authorities with only names and annotations changed. A sign error in both places would produce the same wrong number and pass the gate.
That was a proof defect, not proof that the arithmetic was wrong. The distinction matters because a review should not manufacture a bug to make its criticism exciting.
The review found a concrete behavioral difference too. The compiler rejected an impossible negative witness loss. The pager’s corresponding path did not reject the same result. A later recheck corrected that detail: the pager used a residual form and did have its own negative check. The broader problem survived the correction. No test compared the two arithmetic paths, and both could have shared a systematic error.
Sol used two kinds of separation. The pager received a different calculation: fraction-free Bareiss determinants, direct triple contraction, and an explicit projection residual. The fixture added combinatorial answers and literal complex cases so neither production path could merely agree with the other. Then the test checked the normalized syntax shape of the helpers so a future copy could not pass by changing variable names.
The repaired witness calculation is short enough to show its boundary:
def _witness_loss(target, atom, metric, object_id: str) -> Fraction:
target_norm = _inner(target, metric, target)
atom_norm = _inner(atom, metric, atom)
cross = _inner(atom, metric, target)
if target_norm[1] or atom_norm[1] or atom_norm[0] <= 0:
_reject("CAPABILITY_MISMATCH", object_id, "condition quadratic forms are not positive real values")
loss = target_norm[0] - _absolute_squared(cross) / atom_norm[0]
if loss < 0:
_reject("CAPABILITY_MISMATCH", object_id, "condition witness loss is negative")
return loss
The certificate witness calculation in compiler.py is one implemented path, not the independent oracle by itself. The independent evidence comes from the repaired pager path, the combinatorial fixture, and the syntax-shape assertion that protects the separation.
Kimi’s containment review remained valid. It had attacked pickle material, traversal, templates, custom operators, network declarations, descriptor binding, changed bytes, and candidate-root resumption. Those guards did not need to be reopened because a different boundary had failed. The two reviews had crossed different surfaces.
This is where Drew’s instruction about authorization also entered the source. Opus appended an entry because two earlier messages had paired review with writing. Drew had asked in a particular order. The agent had extended one local permission into a standing instruction. The same inference error appeared in code and in conversation: something plausible was treated as authority because it sat nearby.
The final S19 tree passed 35 of 35 tests in 59.88 seconds and left the ledger clean. The publication guard now checks more than transcription, and the record says exactly what the independent arithmetic proves. Separate files are not automatically independent proof. The calculation has to differ, the oracle has to stand outside both implementations, and the test has to notice if the distinction disappears.
