[splashevolution]

Purpose

Establish the next machine-checked negative result after GREEN-1.

GREEN-1 proves binding correctness relative to a DeviceModel. RED-2 asks whether that also proves representation correctness.

It does not.

Witness

Both candidates use the same GREEN-1-correct resource:

resource = 0x20

but carry different raw payloads:

reference raw value = 250
mutated raw value   = 25

The current GREEN-1 checker sees only the binding and therefore accepts both.

Machine-checked result

reference.resource = mutated.resource
reference.rawValue != mutated.rawValue

GREEN1(reference) = true
GREEN1(mutated)   = true

This establishes:

binding correctness is not representation correctness.

Claim boundary

This PR deliberately does not claim that 250 is semantically correct and 25 is semantically wrong.

The current theory cannot yet state that relation. That is the RED-2 gap.

GREEN-2 constraint

The next step must distinguish the two representations without:

• embedding raw target value 250 in the target-neutral semantic contract;
• trusting the realization generator;
• conflating resource binding with representation;
• adding protocol-state machinery before it is required;
• introducing QEMU/Renode yet.