R12 Certified Language Bridge Boundary

Status: broad bridge rejected. A synthetic residual-state result may cross to language only on machine-checkable deterministic semantic systems whose certificate map reflects every claimed future distinction.

1. Why the current corpus is insufficient

Flattened reasoning rows retain a question, trace, answer, and family, but not the semantic transition states needed to prove future equivalence or derive distinguishing continuations. Answer verification for OpenMath and bounded unit tests for code likewise do not prove residual equivalence.

Therefore a synthetic WGRQ pass cannot be used to relabel the existing SFT mix as causal-state supervision. Provenance-rich sources must be re-extracted into certified bounded systems first.

2. Admissible semantic systems

An admitted domain is a bounded deterministic system

M = (S, E, Q, A, delta, output).

Examples are deliberately narrow:

• exact register programs, finite-field programs, or proof-assistant states;
• total loop-free bit-vector programs or bounded programs with exhaustive/SMT equivalence, not merely passing tests;
• finite Horn/Datalog worlds or finite model sets with canonical closure and exact entailment.

For each world, the builder must produce:

1. distinct histories reaching one certified residual state;
2. a lexically matched mutation in a different residual class;
3. a shortest certificate-backed distinguishing continuation/query;
4. independently worded surfaces that deterministically round-trip to the same typed AST or proof object.

Teacher proposals are allowed only before deterministic verification. Canonical states, class IDs, witnesses, and answers remain training-side metadata and are not emitted as textual packet targets.

3. Bridge non-reflection theorem

Let phi map language histories into a certified synthetic state. If there are histories h,g and a claimed continuation/query (c,q) such that

phi(h) = phi(g)

but the correct language answers after (c,q) differ, then any source-deleted system whose committed packets are interchangeable whenever phi agrees must produce the same output distribution on both histories. On a balanced pair with distinct correct answers, exact accuracy is at most 1/2.

If the two packet-conditioned output distributions differ by at most total variation epsilon, balanced exact accuracy is at most (1+epsilon)/2.

Thus one future-distinguishable collision kills the bridge claim regardless of perfect synthetic performance. The certificate map must be a future-reflecting transition homomorphism over the entire declared continuation/query family.

4. Hard source barrier

A confirmation claim requires process-level deletion:

1. a writer exports only a fixed-size committed packet and exits;
2. source IDs, embeddings, residuals, KV cache, paths, and RNG state die with that process;
3. the continuation/query is sampled only afterward;
4. a fresh reader receives fixed weights, tokenizer, packet, continuation, and query with an empty cache;
5. the reader image has no verifier, solver, retrieval path, source mount, or feedback from scoring.

Training-time non-access is weaker and must be described separately.

5. Acquisition ledger

Count mutually exclusive channels:

• T: every generative-teacher request, including rejected attempts;
• V: certificate checks that only validate a supplied object;
• O: every label-producing transition, readout, equivalence, witness, or target-dependent search query.

Returned bits, query descriptions, adaptive rounds, external search compute, source tokens, and target tokens are also recorded. A solver that discovers a witness is an oracle, not merely a verifier. Shared acquisition cost is charged to every arm; candidate-only adaptive calls disqualify a matched comparison.

6. Decision

Reject a broad synthetic-to-language bridge and any use of the current flat SFT rows as equivalence evidence. Retain a future certificate-bearing language board as a separate phase only after a synthetic source-deleted protocol passes its own controls. One failed domain or one non-reflecting collision rejects the language claim.