Translation converts a frozen domain requirement into a demand the artefact can evaluate. It is the narrowest point in the evaluation's claim, because representability is not binary unless loss is tested explicitly. A demand can be syntactically expressible and still mistranslate its requirement by omitting a condition, adding a stricter one, weakening a prohibition, mapping a condition onto the wrong axis, encoding one branch of a conditional, or substituting an available proxy for the concept actually required.
What each translation records
Every translation names which demand clause answers each frozen atom, or names the smallest construct that would have been needed and is absent. Every demand clause must trace back to an atom: a clause with no antecedent is a condition the source never asked for, and would make any resulting refusal an artefact of the translator's caution. Every relation in the frozen expression must be either represented with the same semantics or explicitly recorded as lost. What is forbidden is silence, because a relation can disappear while every atom is still mapped.
Two cardinality guards apply. One atom mapping to several clauses may add strictness the requirement never asked for; several atoms mapping to one clause may collapse distinct requirements. Neither is forbidden and both require justification. A negative atom must reach an actual exclusion or non-satisfaction rule, since a non-entailment mentioned only in explanatory prose constrains nothing.
Four statuses
A translation is exact, a conservative overconstraint where the demand is stricter than the requirement, an unsafe underconstraint where it is weaker, or unrepresentable where no demand encodes it.
Only exact translations enter the primary discrimination result. A refusal produced by an overconstrained demand is partly an artefact of the translation rather than a finding about the discipline, and pooling the two would make false refusals partly the translator's. Unsafe underconstraints are never adjudicated at all: an admission produced by a demand weaker than the requirement establishes nothing.
The distinction between what a checker can establish and what it cannot is preserved. Mapping completeness is mechanical: every frozen atom accounted for, every clause with an antecedent, every relation represented or recorded as lost. Exactness is a human judgement resting on that mapping and requires a written justification, because no tool can establish that a demand means what a requirement means.
The expressive boundary, established before translating
Before any case was translated, the demand language was read against the frozen expressions and its boundary recorded, so that statuses would follow a stated rule rather than case-by-case judgement.
The language offers per-axis clauses and the kernel conjoins them. There is no disjunction between clauses, no conditional withdrawal of a clause, and no way to assert that a satisfied condition fails to license a conclusion.
That last absence is the important one, and it must not be confused with negation. The requirement that separate devices do not establish independence cannot be translated as a requirement that the devices are not separate: the devices are separate, and that is precisely the situation the requirement addresses. Twenty-two of the thirty-nine frozen expressions use a non-entailment relation of this kind.